Skip to content

Commit 395bd12

Browse files
author
Alex Gryzlov
committed
Comment out exp'_1
1 parent d293e88 commit 395bd12

File tree

1 file changed

+5
-2
lines changed

1 file changed

+5
-2
lines changed

src/Poly.lidr

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1052,8 +1052,11 @@ iterating over a different type: `Nat'` itself is usually problematic.)
10521052
> exp' : (n : Nat' {x}) -> (m : Nat' {x=x->x}) -> Nat' {x}
10531053
> exp' n m = ?exp'_rhs
10541054

1055-
> exp'_1 : exp' two two = plus' two two
1056-
> exp'_1 = ?exp'_1_rhs
1055+
\todo[inline]{This won't typecheck under this signature of `exp` because of 2
1056+
instances of `two`}
1057+
1058+
> -- exp'_1 : exp' two two = plus' two two
1059+
> -- exp'_1 = ?exp'_1_rhs
10571060

10581061
> exp'_2 : exp' three two = plus' (mult' two (mult' two two)) one
10591062
> exp'_2 = ?exp'_2_rhs

0 commit comments

Comments
 (0)