Skip to content

Commit

Permalink
fix: remove reference to canonicalizeHypothesisType, rename `fromLo…
Browse files Browse the repository at this point in the history
…calContext` to `fromMainContext` to reflect that we now use `withMainContext`
  • Loading branch information
alexkeizer committed Sep 26, 2024
1 parent 91f2665 commit 60b484e
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 11 deletions.
9 changes: 3 additions & 6 deletions Tactics/Sym.lean
Original file line number Diff line number Diff line change
Expand Up @@ -244,7 +244,7 @@ elab "explode_step" h_step:term " at " state:term : tactic => withMainContext do
let .fvar stateFVar := state
| throwError "Expected fvar, found {state}"
let stateDecl := (← getLCtx).get! stateFVar
let c ← SymContext.fromLocalContext (some stateDecl.userName)
let c ← SymContext.fromMainContext (some stateDecl.userName)
let _ ← SymM.run c <| explodeStep hStep

/--
Expand Down Expand Up @@ -403,11 +403,8 @@ elab "sym_n" whileTac?:(sym_while)? n:num s:(sym_at)? : tactic => do
omega;
))

let c ← withMainContext <| SymContext.fromLocalContext s
SymM.run' c <| do
-- Context preparation
canonicalizeHypothesisTypes

let c ← SymContext.fromMainContext s
SymM.run' c <| withMainContext' <| do
-- Check pre-conditions
assertStepTheoremsGenerated
let n ← ensureAtMostRunSteps n.getNat
Expand Down
11 changes: 6 additions & 5 deletions Tactics/Sym/Context.lean
Original file line number Diff line number Diff line change
Expand Up @@ -415,14 +415,15 @@ protected def searchFor : SearchLCtxForM SymM Unit := do

return ()

/-- Build a `SymContext` by searching the local context for hypotheses of the
required types (up-to defeq) . The local context is modified to unfold the types
to be syntactically equal to the expected type.
/-- Build a `SymContext` by searching the local context of the main goal for
hypotheses of the required types (up-to defeq).
The local context is modified to unfold the types to be syntactically equal to
the expected types.
If an hypothesis `h_err : r <state> .ERR = None` is not found,
we create a new subgoal of this type
we create a new subgoal of this type.
-/
def fromLocalContext (state? : Option Name) : TacticM SymContext := do
def fromMainContext (state? : Option Name) : TacticM SymContext := do
let msg := m!"Building a `SymContext` from the local context"
withTraceNode `Tactic.sym (fun _ => pure msg) <| withMainContext' do
trace[Tactic.Sym] "state? := {state?}"
Expand Down

0 comments on commit 60b484e

Please sign in to comment.