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

test: macro scopes in Conv.congr (#1955)

Browse source
This commit is contained in:
Mario Carneiro 2022-12-14 17:43:26 +01:00 • committed by GitHub
parent d5fb32a393
commit 52d00e8944
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
tests/lean/conv1.lean
View file

@ -242,3 +242,6 @@ example : ((x + y) + z : Nat) = x + (y + z) := by conv => pattern (occs := 5) _
example : ((x + y) + z : Nat) = x + (y + z) := by conv => pattern (occs := 2 5) _ + _
example : ((x + y) + z : Nat) = x + (y + z) := by conv => pattern (occs := 1 5) _ + _
example : ((x + y) + z : Nat) = x + (y + z) := by conv => pattern (occs := 1 2 5) _ + _
macro "bla" : term => `(?a)
example : 1 = 1 := by conv => apply bla; congr