max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: repeat conv should not auto-close the goal

Browse source
This commit is contained in:
Mario Carneiro 2023-07-25 14:16:55 -04:00 • committed by Mac
parent 53477089fe
commit 776bff1948
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Conv.lean
View file

@ -286,7 +286,7 @@ macro:1 x:conv tk:" <;> " y:conv:0 : conv =>
/-- `repeat convs` runs the sequence `convs` repeatedly until it fails to apply. -/
syntax "repeat " convSeq : conv
macro_rules
| `(conv| repeat $seq) => `(conv| first | ($seq); repeat $seq | rfl)
| `(conv| repeat $seq) => `(conv| first | ($seq); repeat $seq | skip)
/--
`conv => ...` allows the user to perform targeted rewriting on a goal or hypothesis,