| import Lean | |
| open Lean Meta | |
| open PrettyPrinter Delaborator SubExpr in | |
| @[delab fvar] | |
| def delabFVar : Delab := do | |
| let Expr.fvar fvarId ← getExpr | unreachable! | |
| let none := (← getLCtx).find? fvarId | failure | |
| return mkIdent `FREE | |
| #eval do | |
| let e ← withLetDecl `y (mkConst ``Nat) (mkConst ``Nat.zero) fun y => do | |
| let m ← mkFreshExprMVar (mkConst ``Nat) | |
| m.mvarId!.assign y | |
| let e := mkApp2 (mkConst ``Nat.add) m y | |
| -- goal: construct λ y, e | |
| dbg_trace (← ppExpr (← mkLambdaFVars #[y] e)) -- doesn't work: creates let | |
| dbg_trace (← ppExpr (← instantiateMVars <| -- doesn't work: contains free variable | |
| mkLambda `y BinderInfo.default (mkConst ``Nat) (e.abstract #[y]))) | |
| instantiateMVars <| -- doesn't work: contains free variable | |
| mkLambda `y BinderInfo.default (mkConst ``Nat) (e.abstract #[y]) | |
| dbg_trace (← ppExpr e) | |
| #eval | |
| withLetDecl `y (mkConst ``Nat) (mkConst ``Nat.zero) fun y => do | |
| let m ← mkFreshExprMVar (mkConst ``Nat) | |
| m.mvarId!.assign y | |
| let e := mkApp2 (mkConst ``Nat.add) m y | |
| -- goal: construct λ y, e | |
| dbg_trace (← instantiateMVars <| -- doesn't work: contains free variable | |
| mkLambda `y BinderInfo.default (mkConst ``Nat) (← e.abstractM #[y])) | |
| #eval do | |
| let (e, _) ← withLetDecl `y (mkConst ``Nat) (mkConst ``Nat.zero) fun y => do | |
| let m ← mkFreshExprMVar (mkConst ``Nat) (kind := MetavarKind.syntheticOpaque) | |
| let e := mkApp2 (mkConst ``Nat.add) m y | |
| dbg_trace (← ppExpr e) | |
| dbg_trace (← ppExpr (← e.abstractM #[y])) | |
| let e ← instantiateMVars <| -- doesn't work: contains free variable | |
| mkLambda `y BinderInfo.default (mkConst ``Nat) (← e.abstractM #[y]) | |
| m.mvarId!.assign (mkApp2 (mkConst ``Nat.add) y y) | |
| return (e, m) | |
| dbg_trace (← ppExpr (← instantiateMVars e)) |