Merge branch 'develop' into first_part_cleanup

Author: yurrriq

software_foundations.ipkg

@@ -7,6 +7,9 @@ modules    = Basics
            , Tactics
            , Logic
            , IndProp
+           , Maps
+           , ProofObjects
+           , Rel
 
 brief      = "Software Foundations in Idris"
 version    = 0.0.1.0

src/IndProp.lidr

@@ -1268,6 +1268,13 @@ by combining evidence for \idr{Not p} with the \idr{ReflectF} constructor.
 It is easy to formalize this intuition and show that the two statements are
 indeed equivalent:
 
+\todo[inline]{Remove when a release with
+https://github.com/idris-lang/Idris-dev/pull/3925 happens}
+
+> implementation Uninhabited (False = True) where
+>   uninhabited Refl impossible
+>
+
 > iff_reflect : (p <-> (b = True)) -> Reflect p b
 > iff_reflect {b = False} (pb, _) = ReflectF (uninhabited . pb) Refl
 > iff_reflect {b = True} (_, bp) = ReflectT (bp Refl) Refl

src/Makefile

@@ -18,7 +18,10 @@ LIDR_FILES := Preface.lidr \
 	Poly.lidr \
 	Tactics.lidr \
 	Logic.lidr \
-	IndProp.lidr
+	IndProp.lidr \
+	Maps.lidr \
+	ProofObjects.lidr \
+	Rel.lidr
 # TODO: Add more chapters, in order, here.
 
 

src/Maps.lidr

@@ -79,6 +79,21 @@ present purposes you can think of it as just a fancy \idr{Bool}.)
 The following useful property of  \idr{beq_id} follows from an analogous lemma
 about strings:
 
+\todo[inline]{Copied \idr{<->} for now}
+
+> iff : {p,q : Type} -> Type
+> iff {p} {q} = (p -> q, q -> p)
+>
+> syntax [p] "<->" [q] = iff {p} {q}
+>
+
+\todo[inline]{Remove when a release with
+https://github.com/idris-lang/Idris-dev/pull/3925 happens}
+
+> implementation Uninhabited (False = True) where
+>   uninhabited Refl impossible
+>
+
 > beq_id_true_iff : (beq_id x y = True) <-> x = y
 > beq_id_true_iff = (bto, bfro)
 >   where