Skip to content

Commit

Permalink
core: make AliveStatements.lean robust against multiple goals (#301)
Browse files Browse the repository at this point in the history
#225 will fix three statements, one
of which will introduce multiple goals in `AliveStatements.lean`. This
PR makes `AliveStatements.lean` robust against multiple worries by using
`all_goals`.

Thank you @alexkeizer for proposing this.
  • Loading branch information
tobiasgrosser authored May 13, 2024
1 parent fab92c2 commit 47df14a
Show file tree
Hide file tree
Showing 2 changed files with 91 additions and 91 deletions.
Loading

0 comments on commit 47df14a

Please sign in to comment.