Skip to content

Commit 538b0f0

Browse files
author
Alex Gryzlov
committed
mention the Refl lambda issue
1 parent 3f4362c commit 538b0f0

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

src/Logic.lidr

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -316,7 +316,8 @@ $\square$
316316
This is how we use \idr{Not} to state that \idr{0} and \idr{1} are different
317317
elements of \idr{Nat}:
318318

319-
\todo[inline]{Explain \idr{Refl}-lambda syntax and \idr{Uninhabited}}
319+
\todo[inline]{Explain \idr{Refl}-lambda syntax and \idr{Uninhabited}, keep in
320+
mind https://github.com/idris-lang/Idris-dev/issues/3943}
320321

321322
> zero_not_one : Not (Z = S _)
322323
> zero_not_one = \Refl impossible

0 commit comments

Comments
 (0)