Skip to content
This repository was archived by the owner on Feb 26, 2021. It is now read-only.

Commit 74aa142

Browse files
banacornbanacorn
committed
Add Error.IlltypedPattern
1 parent f7c6be6 commit 74aa142

File tree

7 files changed

+245
-183
lines changed

7 files changed

+245
-183
lines changed

‎lib/parser/agda.js‎

Lines changed: 1 addition & 1 deletion
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎lib/parser/error.js‎

Lines changed: 64 additions & 55 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎lib/view/component/Error.js‎

Lines changed: 7 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎spec/error/IlltypedPattern.agda‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
-- https://github.com/agda/agda/blob/acc9bd12b455ecfa118381cca4cd8f9522ef96c8/test/Fail/IlltypedPattern.agda
2+
module IlltypedPattern where
3+
4+
data Nat : Set where
5+
zero : Nat
6+
suc : Nat -> Nat
7+
8+
f : (A : Set) -> A -> A
9+
f A zero = zero
10+
11+
-- IlltypedPattern.agda:9,5-9
12+
-- Type mismatch
13+
-- when checking that the pattern zero has type A

0 commit comments

Comments
 (0)