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

chore: fix test

Browse source 
`set_option` command after `by` tactic block is ambiguous.
We need to indent or use `{ ... }`.

cc @Kha
This commit is contained in:
Leonardo de Moura 2021-03-06 16:46:18 -08:00
parent 061b9bf60f
commit 6ec5c1de54
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/lean/hygienicIntro.lean
View file

@ -20,9 +20,9 @@ apply h1;
assumption
example {p q : Prop} (h₁ : p → q) (h₂ : p ∨ q) : q := by
cases h₂;
{ apply h₁; exact h }; -- error "unknown identifier"
exact h
cases h₂;
{ apply h₁; exact h }; -- error "unknown identifier"
exact h
set_option hygienicIntro false in
example {p q : Prop} (h₁ : p → q) (h₂ : p ∨ q) : q := by

2
tests/lean/hygienicIntro.lean.expected.out
View file

@ -1,2 +1,2 @@
hygienicIntro.lean:14:6-14:9: error: unknown identifier 'a_1'
hygienicIntro.lean:24:18-24:19: error: unknown identifier 'h'
hygienicIntro.lean:24:20-24:21: error: unknown identifier 'h'