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

chore: fix mkForbiddenSet

Browse source
This commit is contained in:
Leonardo de Moura 2021-03-27 14:59:05 -07:00
parent 2e5a9d9c99
commit b32b542a85
2 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Tactic/Induction.lean
View file

@ -266,7 +266,7 @@ where
| [] => return s
| fvarId::todo =>
if s.contains fvarId then
return s
loop todo s
else
let (todo, s) ← visit fvarId todo <| s.insert fvarId
loop todo s

8
tests/lean/run/inductionAltExplicit.lean
View file

@ -11,8 +11,8 @@ def lexAccessible1 {ra : α → α → Prop} {rb : β → β → Prop} (aca : (a
apply Acc.intro (xa, xb)
intro p lt
cases lt with
| left b1 b2 h => apply iha _ h _ (aca _ h)
| @right a b1 b2 h => apply ihb _ h (acb _ h)
| left b1 b2 h => apply iha _ h
| @right a b1 b2 h => apply ihb _ h
def lexAccessible2 {ra : α → α → Prop} {rb : β → β → Prop} (aca : (a : α) → Acc ra a) (acb : (b : β) → Acc rb b) (a : α) (b : β) : Acc (Lex ra rb) (a, b) := by
induction (aca a) generalizing b with
@ -22,5 +22,5 @@ def lexAccessible2 {ra : α → α → Prop} {rb : β → β → Prop} (aca : (a
apply Acc.intro (xa, xb)
intro p lt
cases lt with
| @left a1 b1 a2 b2 h => apply iha _ h _ (aca _ h)
| right _ h => apply ihb _ h (acb _ h)
| @left a1 b1 a2 b2 h => apply iha _ h
| right _ h => apply ihb _ h