Skip to content

Commit

Permalink
fix: inferStatePrefix... should default to s1 as the first interm…
Browse files Browse the repository at this point in the history
…ediate state.

This means setting `currentStateNumber := 0`
  • Loading branch information
alexkeizer committed Sep 26, 2024
1 parent 0194790 commit 3d79e30
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Tactics/SymContext.lean
Original file line number Diff line number Diff line change
Expand Up @@ -247,7 +247,7 @@ Falling back to the default numbering scheme, \
with `s1` as the first new intermediate state"
modifyThe SymContext ({ · with
state_prefix := "s",
currentStateNumber := 1 })
currentStateNumber := 0 })

/-- Annotate any errors thrown by `k` with a local variable (and its type) -/
private def withErrorContext (name : Name) (type? : Option Expr) (k : MetaM α) :
Expand Down

0 comments on commit 3d79e30

Please sign in to comment.