Auguste Poiroux

I have found that this can be overcome by encapsulating the partial proof with `(\n

Hi, Happy new year! So, unfortunately, in this context, it seems that this makes the `exact?` tactic slightly dangerous to use as it will "prove" anything: ``` {"cmd": "theorem ex...

Interesting, thanks! Having the definition in `constants` is probably useful/necessary for the `pickle` feature.

Tests corresponding to the various minimal cases mentioned in @Kripner message have been added to #63. So far, it seems that only the following self-application example is not caught: ```lean...

@RexWzh this example is interesting, and #63 incorrectly rejects it during kernel check. It seems related to the other problem you mentioned earlier in this discussion about set options that...

I think it is also important to keep in mind that Lean REPL is a general tool. While most of us use it in an AI4Math context, there are other...

@RexWzh Just pushed a new PR #82 which should fix the `set_config` issues. Your miniF2F example makes the memory explodes just like in command mode.

@RexWzh Which commit did you use for this example? On the master branch, when I try your example: ``` {"cmd": "example : true := by sorry"} {"tactic": "let p :...

This is an interesting feature in my opinion. REPL has extraction capabilities centered around tactics, and I believe that adding some for declarations could be nice. https://github.com/leanprover-community/repl/pull/96 is related to...

Interesting, do you have a minimal Github Lean project with canonical set up? I am interested in reproducing your issue. Are you on Windows? I see a `canonical_lean.dll`