lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

Add option `pp.beta`

Open leodemoura opened this issue 3 years ago • 1 comments

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 avatar Oct 06 '21 20:10 leodemoura

Marked it with lean4_release because Lean3 has this feature.

leodemoura avatar Jun 01 '22 23:06 leodemoura