Amitayush Thakur

Issue while installing `Zarith`

4

When I run `opam install zarith`. It fails with the following error: ``` The following actions will be performed: ∗ install zarith 1.13 Processing actions ⬇ retrieved zarith.1.13 (cached) [ERROR]...

[BUG] REPL accepts incorrect proofs

36

I found a peculiar bug in REPL, where it can accept any proof that applies the theorem itself. Example: ``` {"cmd": "theorem test (p q : Prop) (hp : p)...

Issues while executing tactics with `;` in them.

2

I was trying to execute the following theorem via REPL: ``` theorem ftaylorSeriesWithin_univ : ftaylorSeriesWithin 𝕜 f univ = ftaylorSeries 𝕜 f := by sorry ``` .This theorem can be...