Open Seasawher opened 5 days ago
import Lean open Lean Elab Term #eval show TermElabM _ from do let stx : Syntax ← `(∀ (a : Prop) (b : Prop), a ∨ b → b → a ∧ a) let expr ← elabTermAndSynthesize stx none logInfo expr