l3-ENSL/pieuvre
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Add more bad 8pus tests

Browse Source
This commit is contained in:
augustin64 2024-05-20 14:52:19 +02:00
parent e6680b181c
commit 6313af9346
3 changed files with 9 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
tests/8pus/bad/badHtype_exact.8pus Normal file
View File

@ -0,0 +1,5 @@
Goal A -> B -> A.
intro.
exact H1.
exact H0.
Qed.

7
tests/8pus/bad/badtype_exact.8pus
View File

@ -1,5 +1,2 @@
Goal A -> B -> A. Goal A -> B.
intro. exact (fun (x:A) => x).
exact H1.
exact H0.
Qed.

2
tests/8pus/bad/notype_exact.8pus Normal file
View File

@ -0,0 +1,2 @@
Goal A -> B.
exact (fun (x:A) => y).