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

test: add second example for issue #423

Browse source
This commit is contained in:
Leonardo de Moura 2021-04-25 10:35:23 -07:00
parent b670d6b8d7
commit 2cbdd637c7
2 changed files with 26 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/423.lean
View file

@ -1,3 +1,5 @@
universe u
#check fun {T : Sort u} (a : T) => a + 0
#check fun {T : Sort u} (a : T) [Add T] [OfNat T 0] => a + 0

24
tests/lean/423.lean.expected.out
View file

@ -6,3 +6,27 @@ has type
T : Sort u
but is expected to have type
Nat : Type
423.lean:5:33-5:38: error: application type mismatch
Add T
argument
T
has type
Sort u : Type u
but is expected to have type
Type ?u : Type (?u + 1)
423.lean:5:41-5:50: error: application type mismatch
OfNat T
argument
T
has type
Sort u : Type u
but is expected to have type
Type ?u : Type (?u + 1)
423.lean:5:55-5:60: error: application type mismatch
HAdd.hAdd a
argument
a
has type
T : Sort u
but is expected to have type
Nat : Type