Add option `pp.beta` - Githubissues

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.77k stars 430 forks source link

Add option `pp.beta` #715

Closed leodemoura closed 1 year ago

leodemoura commented 3 years ago

When pp.beta is set to true, the pretty-printer (delaborator) should apply beta reduction. Lean 3 implements this feature, but we had not implemented it yet in Lean 4.

leodemoura commented 2 years ago

Marked it with lean4_release because Lean3 has this feature.