summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Diverge
diff options
context:
space:
mode:
authorSon Ho2023-07-10 15:06:12 +0200
committerSon Ho2023-07-10 15:06:12 +0200
commit7206b48a73d6204baea99f4f4675be2518a8f8c2 (patch)
tree017aa1132948c51498bf529a42c48729bed0a6aa /backends/lean/Base/Diverge
parentd9a11b312ef0df13795d9a1982ca1cd2eba0e124 (diff)
Start working on the progress tactic
Diffstat (limited to 'backends/lean/Base/Diverge')
-rw-r--r--backends/lean/Base/Diverge/Elab.lean17
1 files changed, 1 insertions, 16 deletions
diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean
index 96f7abc0..f109e847 100644
--- a/backends/lean/Base/Diverge/Elab.lean
+++ b/backends/lean/Base/Diverge/Elab.lean
@@ -14,8 +14,8 @@ namespace Diverge
syntax (name := divergentDef)
declModifiers "divergent" "def" declId ppIndent(optDeclSig) declVal : command
-open Utils
open Lean Elab Term Meta Primitives Lean.Meta
+open Utils
/- The following was copied from the `wfRecursion` function. -/
@@ -47,21 +47,6 @@ def getSigmaTypes (ty : Expr) : MetaM (Expr × Expr) := do
else
pure (args.get! 0, args.get! 1)
-/- Like `lambdaTelescopeN` but only destructs a fixed number of lambdas -/
-def lambdaTelescopeN (e : Expr) (n : Nat) (k : Array Expr → Expr → MetaM α) : MetaM α :=
- lambdaTelescope e fun xs body => do
- if xs.size < n then throwError "lambdaTelescopeN: not enough lambdas";
- let xs := xs.extract 0 n
- let ys := xs.extract n xs.size
- let body ← mkLambdaFVars ys body
- k xs body
-
-/- Like `lambdaTelescope`, but only destructs one lambda
- TODO: is there an equivalent of this function somewhere in the
- standard library? -/
-def lambdaOne (e : Expr) (k : Expr → Expr → MetaM α) : MetaM α :=
- lambdaTelescopeN e 1 λ xs b => k (xs.get! 0) b
-
/- Generate a Sigma type from a list of *variables* (all the expressions
must be variables).