diff options
author | Son HO | 2024-02-03 00:23:30 +0100 |
---|---|---|
committer | GitHub | 2024-02-03 00:23:30 +0100 |
commit | eb8bddcbd120f666f74023de9a23c48e1a55833d (patch) | |
tree | 1d8290e4b947e431c3d8d3a9f8575f23c3afe5e1 /backends/lean/Base/Progress | |
parent | 0960ad16838a43da3746f47cf5b640bfbb783d84 (diff) | |
parent | 9cc912e2414870df85ffc4dd346ade5dba2b5c37 (diff) |
Merge pull request #68 from AeneasVerif/son/update_lean
Update Lean to v4.6.0-rc1
Diffstat (limited to 'backends/lean/Base/Progress')
-rw-r--r-- | backends/lean/Base/Progress/Base.lean | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean index a64212a5..03c80a42 100644 --- a/backends/lean/Base/Progress/Base.lean +++ b/backends/lean/Base/Progress/Base.lean @@ -139,12 +139,12 @@ def getPSpecFunArgsExpr (isGoal : Bool) (th : Expr) : MetaM Expr := -- pspec attribute structure PSpecAttr where attr : AttributeImpl - ext : DiscrTreeExtension Name true + ext : DiscrTreeExtension Name deriving Inhabited /- The persistent map from expressions to pspec theorems. -/ initialize pspecAttr : PSpecAttr ← do - let ext ← mkDiscrTreeExtention `pspecMap true + let ext ← mkDiscrTreeExtention `pspecMap let attrImpl : AttributeImpl := { name := `pspec descr := "Marks theorems to use with the `progress` tactic" @@ -160,7 +160,9 @@ initialize pspecAttr : PSpecAttr ← do let fExpr ← getPSpecFunArgsExpr false thDecl.type trace[Progress] "Registering spec theorem for {fExpr}" -- Convert the function expression to a discrimination tree key - DiscrTree.mkPath fExpr) + -- We use the default configuration + let config : WhnfCoreConfig := {} + DiscrTree.mkPath fExpr config) let env := ext.addEntry env (fKey, thName) setEnv env trace[Progress] "Saved the environment" @@ -170,9 +172,11 @@ initialize pspecAttr : PSpecAttr ← do pure { attr := attrImpl, ext := ext } def PSpecAttr.find? (s : PSpecAttr) (e : Expr) : MetaM (Array Name) := do - (s.ext.getState (← getEnv)).getMatch e + -- We use the default configuration + let config : WhnfCoreConfig := {} + (s.ext.getState (← getEnv)).getMatch e config -def PSpecAttr.getState (s : PSpecAttr) : MetaM (DiscrTree Name true) := do +def PSpecAttr.getState (s : PSpecAttr) : MetaM (DiscrTree Name) := do pure (s.ext.getState (← getEnv)) def showStoredPSpec : MetaM Unit := do |