We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
Uninhabited (False = True)
1 parent 87a6a94 commit 67310bdCopy full SHA for 67310bd
src/IndProp.lidr
@@ -1305,6 +1305,13 @@ by combining evidence for \idr{Not p} with the \idr{ReflectF} constructor.
1305
It is easy to formalize this intuition and show that the two statements are
1306
indeed equivalent:
1307
1308
+\todo[inline]{Remove when a release with
1309
+https://github.com/idris-lang/Idris-dev/pull/3925 happens}
1310
+
1311
+> implementation Uninhabited (False = True) where
1312
+> uninhabited Refl impossible
1313
+>
1314
1315
> iff_reflect : (p <-> (b = True)) -> Reflect p b
1316
> iff_reflect {b = False} (pb, _) = ReflectF (uninhabited . pb) Refl
1317
> iff_reflect {b = True} (_, bp) = ReflectT (bp Refl) Refl
0 commit comments