JetBrains / Arend

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

Pretty printer for let under WHNF #216

Open ice1000 opened 4 years ago

ice1000 commented 4 years ago

I did the following in the REPL:

>\let | x => 5 | y => 2 \in \lam z => x + y + z

  \let | x => 5
       | y => 2
  \in (+) (x + y)
>:n whnf
>\let | x => 5 | y => 2 \in \lam z => x + y + z
(+) (x + y)
>:n nf
>\let | x => 5 | y => 2 \in \lam z => x + y + z
(+) 7
>:q

I don't like it prints (+) (x + y) on WHNF where information on x and y are lost