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. (#199)

### Description:

We claim in the error that we fall back to `s1` as the first
intermediate state if we can't infer anything.
However, the implementation actually used `s2`. 

This PR fixes that by setting `currentStateNumber := 0` in the fallback
case. The off-by-one behaviour is because this number is incremented
*before* it's used to generate a new state.

### Testing:

What tests have been run? Did `make all` succeed for your changes? Was
conformance testing successful on an Aarch64 machine? Yes

### License:

By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.
  • Loading branch information
alexkeizer authored Sep 27, 2024
1 parent 0194790 commit 06bc3ec
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 06bc3ec

Please sign in to comment.