summaryrefslogtreecommitdiff
path: root/backends/lean/Base
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean/Base')
-rw-r--r--backends/lean/Base/Arith.lean44
1 files changed, 21 insertions, 23 deletions
diff --git a/backends/lean/Base/Arith.lean b/backends/lean/Base/Arith.lean
index 6339f218..d4611deb 100644
--- a/backends/lean/Base/Arith.lean
+++ b/backends/lean/Base/Arith.lean
@@ -168,36 +168,27 @@ elab "list_local_decls_1" : tactic =>
| .some _ => dbg_trace f!" Scalar expression"; pure r
| _ => dbg_trace f!" Not a scalar"; pure .none
pure ()
- -- match ← Lean.observing? (Lean.Meta.mkAppM `Scalar.toInt #[decl.toExpr]) with
- -- | .none => dbg_trace f!" Not a scalar"
- -- | .some _ => dbg_trace f!" Scalar expression"
-#check Lean.Environment.addDecl
-#check Expr
-#check LocalContext
-#check MVarId
-#check Lean.Elab.Tactic.setGoals
-#check Lean.Elab.Tactic.Context
-#check withLocalDecl
-#check Lean.MVarId.assert
-#check LocalDecl
-
--- Insert x = 3 in the context
-elab "custom_let" : tactic =>
+def evalCustomLet (name : Name) (val : Syntax) : Tactic.TacticM Unit :=
-- I don't think we need that
Lean.Elab.Tactic.withMainContext do
--
- let type := (Expr.const `Nat [])
- let val : Expr := .lit (.natVal 3)
- let n := `x -- the name is "x"
- withLetDecl n type val fun nval => do
+ let val ← elabTerm val .none
+ let type ← inferType val
+ -- In some situations, the type will be left as a metavariable (for instance,
+ -- if the term is `3`, Lean has the choice between `Nat` and `Int` and will
+ -- not choose): we force the instantiation of the meta-variable
+ synthesizeSyntheticMVarsUsingDefault
+ -- Insert the new declaration
+ withLetDecl name type val fun nval => do
-- For debugging
let lctx ← Lean.MonadLCtx.getLCtx
let fid := nval.fvarId!
let decl := lctx.get! fid
- dbg_trace f!" nval: \"{decl.userName}\" ({nval}) : {decl.type} := {decl.value}"
+ -- Remark: logInfo instantiates the mvars (contrary to dbg_trace):
+ logInfo m!" new decl: \"{decl.userName}\" ({nval}) : {decl.type} := {decl.value}"
--
- -- Tranform the main goal `m0?` to `let x = nval in m1?`
+ -- Tranform the main goal `?m0` to `let x = nval in ?m1`
let mvarId ← Tactic.getMainGoal
let newMVar ← mkFreshExprSyntheticOpaqueMVar (← mvarId.getType)
let newVal ← mkLetFVars #[nval] newMVar
@@ -211,11 +202,18 @@ elab "custom_let" : tactic =>
-- we focused on the current goal
Lean.Elab.Tactic.setGoals [newMVar.mvarId!]
+elab "custom_let " n:ident " := " v:term : tactic =>
+ evalCustomLet n.getId v
+
+-- Insert x = 3 in the context
+elab "custom_let " n:ident " := " v:term : tactic =>
+ evalCustomLet n.getId v
+
example : Nat := by
- custom_let
+ custom_let x := 4
apply x
example (x : Bool) : Nat := by
- cases x <;> custom_let <;> apply x
+ cases x <;> custom_let x := 3 <;> apply x
end Arith