Skip to content

Commit 3bf925f

Browse files
committed
fix failing tests
1 parent 5c816c6 commit 3bf925f

File tree

2 files changed

+3
-3
lines changed

2 files changed

+3
-3
lines changed

tests/lean/binrelTypeMismatch.lean.expected.out

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,11 +10,11 @@ has type
1010
Prop : Type
1111
but is expected to have type
1212
Bool : Type
13-
Prop → sorry : Sort (imax 1 u_1)
13+
Prop → sorry : Sort u_1
1414
binrelTypeMismatch.lean:20:27-20:28: error: type mismatch
1515
p
1616
has type
1717
Prop : Type
1818
but is expected to have type
1919
Bool : Type
20-
Prop → sorry : Sort (imax 1 u_1)
20+
Prop → sorry : Sort u_1

tests/lean/run/issue4726.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
-- A refexive type, with multiple parameters to make sure
33
-- we get the order right
44

5-
inductive N where
5+
inductive N : Type where
66
| cons : (Nat -> Bool → N) -> N
77

88

0 commit comments

Comments
 (0)