repl

repl copied to clipboard

Failed to input the tactics step-by-step within a case block

3

First thanks for such excellent tools! I'm testing repl to see if I can enter the tactics one-by-one so that I can get state information within each step. When I...

ohyeat

Python package

3

Adds python interface via a package called `pylean`. See `README.md` for usage instructions. Unit tests in `pylean/tests`.

zhangir-azerbayev

Repl doesn't return any output?

7

I am trying to use the repl, I have no idea how is it supposed to work but I receive no output ``` > lake exe repl { "cmd" :...

Kreijstal

Iterative execution of proofs

2

A common use case for the `repl` is writing proofs tactic by tactic. Currently, this requires re-executing the entire head of the source file. It would be great if we...

zhangir-azerbayev

We will need to do further inspection of the `InfoTree`s to find these, but shouldn't be hard.

kim-em

fix: duplicated and misaligned messages and info trees in output

1

Fixes #40

utensil

Messages accumulate with wrong positions

2

When given multiple inputs that have messages in outputs, it seems that `repl` will accumulate these messages for later outputs, particularly, these messages are marked with positions from previous inputs,...

utensil

Questions from a lean4 noob... Should you include the imports in the lean file sent to the REPL? Is there a way to automatically detect which imports to add given...

Manuscrit

current repl maybe cannot recognize mathcal letter?

7

When I was testing repl using the following example (it's actually the predefined theorem ```Metric.uniformity_basis_dist``` in mathlib4 ```Mathlib/Topology/MetricSpace/PseudoMetric.lean```): ```bash import Mathlib open Set Filter TopologicalSpace Bornology open scoped BigOperators ENNReal...

ohyeat

[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)...

amit9oct