JetBrains / Arend

The Arend Proof Assistant
https://arend-lang.github.io/
Apache License 2.0
694 stars 33 forks source link

\let definitions in REPL #289

Open valis opened 3 years ago

valis commented 3 years ago

Allow let definitions in REPL. E.g.,

> \let x => 3
> x + x
6
ice1000 commented 3 years ago

First we need to be able to parse \let x => 3 as an individual expression I gues

valis commented 3 years ago

It is an individual expression. It's equivalent to \let x => 3 \in {?}.