Merge pull request #1619 from ahmadsalim/feature/renamevoid

Removed `_|_` as a built in declaration and renamed it to `Void`

Author: edwinb

benchmarks/quasigroups/Solver.idr

@@ -103,8 +103,8 @@ legalVal b (x, y) v =
 Filled : Cell n -> Type
 --Filled {n=n} x = Not (Empty x) -- TODO: Find out why this doesn't work
 Filled {n=n} = (\x => Not (Empty x))
---Filled {n=n} x = the (Maybe (Fin n)) Nothing = x -> _|_
---Filled {n=n} = \x => the (Maybe (Fin n)) Nothing = x -> _|_
+--Filled {n=n} x = the (Maybe (Fin n)) Nothing = x -> Void
+--Filled {n=n} = \x => the (Maybe (Fin n)) Nothing = x -> Void
 
 filled : (cell : Cell n) -> Dec (Filled cell)
 filled Nothing = No (\f => f Refl)

libs/base/Control/Isomorphism.idr

@@ -70,21 +70,21 @@ eitherAssoc = MkIso eitherAssoc1 eitherAssoc2 ok1 ok2
         ok2 (Right x) = Refl
 
 ||| Disjunction with false is a no-op
-eitherBotLeft : Iso (Either _|_ a) a
+eitherBotLeft : Iso (Either Void a) a
 eitherBotLeft = MkIso to from ok1 ok2
-  where to : Either _|_ a -> a
-        to (Left x) = FalseElim x
+  where to : Either Void a -> a
+        to (Left x) = void x
         to (Right x) = x
-        from : a -> Either _|_ a
+        from : a -> Either Void a
         from = Right
         ok1 : (x : a) -> to (from x) = x
         ok1 x = Refl
-        ok2 : (x : Either _|_ a) -> from (to x) = x
-        ok2 (Left x) = FalseElim x
+        ok2 : (x : Either Void a) -> from (to x) = x
+        ok2 (Left x) = void x
         ok2 (Right x) = Refl
 
 ||| Disjunction with false is a no-op
-eitherBotRight : Iso (Either a _|_) a
+eitherBotRight : Iso (Either a Void) a
 eitherBotRight = isoTrans eitherComm eitherBotLeft
 
 ||| Isomorphism is a congruence with regards to disjunction
@@ -145,11 +145,11 @@ pairUnitLeft : Iso ((), a) a
 pairUnitLeft = isoTrans pairComm pairUnitRight
 
 ||| Conjunction preserves falsehood
-pairBotLeft : Iso (_|_, a) _|_
-pairBotLeft = MkIso fst FalseElim (\x => FalseElim x) (\y => FalseElim (fst y))
+pairBotLeft : Iso (Void, a) Void
+pairBotLeft = MkIso fst void (\x => void x) (\y => void (fst y))
 
 ||| Conjunction preserves falsehood
-pairBotRight : Iso (a, _|_) _|_
+pairBotRight : Iso (a, Void) Void
 pairBotRight = isoTrans pairComm pairBotLeft
 
 ||| Isomorphism is a congruence with regards to conjunction
@@ -240,9 +240,9 @@ maybeEither = MkIso to from iso1 iso2
         iso2 (Just x) = Refl
 
 ||| Maybe of void is just unit
-maybeVoidUnit : Iso (Maybe _|_) ()
-maybeVoidUnit = (Maybe _|_)     ={ maybeEither   }=
-                (Either _|_ ()) ={ eitherBotLeft }=
+maybeVoidUnit : Iso (Maybe Void) ()
+maybeVoidUnit = (Maybe Void)     ={ maybeEither   }=
+                (Either Void ()) ={ eitherBotLeft }=
                 ()              QED
 
 eitherMaybeLeftMaybe : Iso (Either (Maybe a) b) (Maybe (Either a b))
@@ -280,16 +280,16 @@ maybeIsoS = MkIso forth back fb bf
         fb FZ = Refl
         fb (FS x) = Refl
 
-finZeroBot : Iso (Fin 0) _|_
-finZeroBot = MkIso (\x => FalseElim (uninhabited x))
-                   (\x => FalseElim x)
-                   (\x => FalseElim x)
-                   (\x => FalseElim (uninhabited x))
+finZeroBot : Iso (Fin 0) Void
+finZeroBot = MkIso (\x => void (uninhabited x))
+                   (\x => void x)
+                   (\x => void x)
+                   (\x => void (uninhabited x))
 
 eitherFinPlus : Iso (Either (Fin m) (Fin n)) (Fin (m + n))
 eitherFinPlus {m = Z} {n=n} =
   (Either (Fin 0) (Fin n)) ={ eitherCongLeft finZeroBot }=
-  (Either _|_ (Fin n))     ={ eitherBotLeft             }=
+  (Either Void (Fin n))     ={ eitherBotLeft             }=
   (Fin n)                  QED
 eitherFinPlus {m = S k} {n=n} =
   (Either (Fin (S k)) (Fin n))     ={ eitherCongLeft (isoSym maybeIsoS) }=
@@ -302,8 +302,8 @@ eitherFinPlus {m = S k} {n=n} =
 finPairTimes : Iso (Fin m, Fin n) (Fin (m * n))
 finPairTimes {m = Z} {n=n} =
   (Fin Z, Fin n) ={ pairCongLeft finZeroBot }=
-  (_|_, Fin n)   ={ pairBotLeft             }=
-  _|_            ={ isoSym finZeroBot       }=
+  (Void, Fin n)   ={ pairBotLeft             }=
+  Void            ={ isoSym finZeroBot       }=
   (Fin Z)        QED
 finPairTimes {m = S k} {n=n} =
   (Fin (S k), Fin n)                  ={ pairCongLeft (isoSym maybeIsoS)      }=

libs/base/Data/Heap.idr

@@ -135,12 +135,12 @@ instance Ord a => JoinSemilattice (MaxiphobicHeap a) where
 -- Properties
 --------------------------------------------------------------------------------
 
-total absurdBoolDischarge : False = True -> _|_
+total absurdBoolDischarge : False = True -> Void
 absurdBoolDischarge p = replace {P = disjointTy} p ()
   where
     total disjointTy : Bool -> Type
     disjointTy False  = ()
-    disjointTy True   = _|_
+    disjointTy True   = Void
 
 total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z
 isEmptySizeZero Empty          p = Refl
@@ -169,7 +169,7 @@ mergePreservesValidHeaps (Node ls ll le lr) (Node rs rl re rr) lp rp =
 
 isEmptySizeZeroNodeAbsurd = proof {
     intros;
-    refine FalseElim;
+    refine void;
     refine absurdBoolDischarge;
     exact p;
 }

libs/base/Data/List.idr

@@ -32,7 +32,7 @@ isElem x (y :: xs) with (decEq x y)
     isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)
       where
         mkNo : {xs' : List a} ->
-               ((x' = y') -> _|_) -> (Elem x' xs' -> _|_) ->
-               Elem x' (y' :: xs') -> _|_
+               ((x' = y') -> Void) -> (Elem x' xs' -> Void) ->
+               Elem x' (y' :: xs') -> Void
         mkNo f g Here = f Refl
         mkNo f g (There x) = g x

libs/base/Data/Vect.idr

@@ -15,7 +15,7 @@ data Elem : a -> Vect k a -> Type where
      There : Elem x xs -> Elem x (y::xs)
 
 ||| Nothing can be in an empty Vect
-noEmptyElem : {x : a} -> Elem x [] -> _|_
+noEmptyElem : {x : a} -> Elem x [] -> Void
 noEmptyElem Here impossible
 
 ||| An item not in the head and not in the tail is not in the Vect at all

libs/base/Data/Vect/Quantifiers.idr

@@ -10,7 +10,7 @@ data Any : (P : a -> Type) -> Vect n a -> Type where
   There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)
 
 ||| No element of an empty vector satisfies any property
-anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_
+anyNilAbsurd : {P : a -> Type} -> Any P Nil -> Void
 anyNilAbsurd (Here _) impossible
 anyNilAbsurd (There _) impossible
 
@@ -48,11 +48,11 @@ negAnyAll : {P : a -> Type} -> {xs : Vect n a} -> Not (Any P xs) -> All (\x => N
 negAnyAll {xs=Nil} _ = Nil
 negAnyAll {xs=(x::xs)} f = (\x => f (Here x)) :: negAnyAll (\x => f (There x))
 
-notAllHere : {P : a -> Type} -> {xs : Vect n a} -> Not (P x) -> All P (x :: xs) -> _|_
+notAllHere : {P : a -> Type} -> {xs : Vect n a} -> Not (P x) -> All P (x :: xs) -> Void
 notAllHere _ Nil impossible
 notAllHere np (p :: _) = np p
 
-notAllThere : {P : a -> Type} -> {xs : Vect n a} -> Not (All P xs) -> All P (x :: xs) -> _|_
+notAllThere : {P : a -> Type} -> {xs : Vect n a} -> Not (All P xs) -> All P (x :: xs) -> Void
 notAllThere _ Nil impossible
 notAllThere np (_ :: ps) = np ps
 

libs/base/Data/ZZ.idr

@@ -122,7 +122,7 @@ posInjective Refl = Refl
 negSInjective : NegS n = NegS m -> n = m
 negSInjective Refl = Refl
 
-posNotNeg : Pos n = NegS m -> _|_
+posNotNeg : Pos n = NegS m -> Void
 posNotNeg Refl impossible
 
 -- Decidable equality

libs/base/Decidable/Order.idr

@@ -84,15 +84,15 @@ LTEIsAntisymmetric (S n) (S m) (LTESucc mLTEn) (LTESucc nLTEm) with (LTEIsAntisy
 instance Poset Nat LTE where
   antisymmetric = LTEIsAntisymmetric
 
-total zeroNeverGreater : {n : Nat} -> LTE (S n) Z -> _|_
+total zeroNeverGreater : {n : Nat} -> LTE (S n) Z -> Void
 zeroNeverGreater {n} LTEZero     impossible
 zeroNeverGreater {n} (LTESucc _) impossible
 
 total zeroAlwaysSmaller : {n : Nat} -> LTE Z n
 zeroAlwaysSmaller = LTEZero
 
-total ltesuccinjective : {n : Nat} -> {m : Nat} -> (LTE n m -> _|_) -> LTE (S n) (S m) -> _|_
-ltesuccinjective {n} {m} disprf (LTESucc nLTEm) = FalseElim (disprf nLTEm)
+total ltesuccinjective : {n : Nat} -> {m : Nat} -> (LTE n m -> Void) -> LTE (S n) (S m) -> Void
+ltesuccinjective {n} {m} disprf (LTESucc nLTEm) = void (disprf nLTEm)
 ltesuccinjective {n} {m} disprf LTEZero         impossible
 
 

libs/prelude/Builtins.idr

@@ -29,8 +29,14 @@ data Pair : (A : Type) -> (B : Type) -> Type where
 data Sigma : (a : Type) -> (P : a -> Type) -> Type where
     MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P
 
-||| The eliminator for the empty type.
-FalseElim : _|_ -> a
+||| The empty type, also known as the trivially false proposition.
+|||
+||| Use `void` or `absurd` to prove anything if you have a variable of type `Void` in scope. 
+%elim data Void : Type where    
+    
+||| The eliminator for the `Void` type.
+void : Void -> a
+void {a} v = elim_for Void (\_ => a) v
 
 ||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
 data Symbol_ : String -> Type where

libs/prelude/Decidable/Equality.idr

@@ -13,7 +13,7 @@ import Prelude.Maybe
 --------------------------------------------------------------------------------
 
 ||| The negation of equality is symmetric (follows from symmetry of equality)
-total negEqSym : {a : t} -> {b : t} -> (a = b -> _|_) -> (b = a -> _|_)
+total negEqSym : {a : t} -> {b : t} -> (a = b -> Void) -> (b = a -> Void)
 negEqSym p h = p (sym h)
 
 
@@ -36,7 +36,7 @@ instance DecEq () where
 --------------------------------------------------------------------------------
 -- Booleans
 --------------------------------------------------------------------------------
-total trueNotFalse : True = False -> _|_
+total trueNotFalse : True = False -> Void
 trueNotFalse Refl impossible
 
 instance DecEq Bool where
@@ -49,7 +49,7 @@ instance DecEq Bool where
 -- Nat
 --------------------------------------------------------------------------------
 
-total OnotS : Z = S n -> _|_
+total OnotS : Z = S n -> Void
 OnotS Refl impossible
 
 instance DecEq Nat where
@@ -64,7 +64,7 @@ instance DecEq Nat where
 -- Maybe
 --------------------------------------------------------------------------------
 
-total nothingNotJust : {x : t} -> (Nothing {a = t} = Just x) -> _|_
+total nothingNotJust : {x : t} -> (Nothing {a = t} = Just x) -> Void
 nothingNotJust Refl impossible
 
 instance (DecEq t) => DecEq (Maybe t) where
@@ -79,7 +79,7 @@ instance (DecEq t) => DecEq (Maybe t) where
 -- Either
 --------------------------------------------------------------------------------
 
-total leftNotRight : {x : a} -> {y : b} -> Left {b = b} x = Right {a = a} y -> _|_
+total leftNotRight : {x : a} -> {y : b} -> Left {b = b} x = Right {a = a} y -> Void
 leftNotRight Refl impossible
 
 instance (DecEq a, DecEq b) => DecEq (Either a b) where
@@ -96,7 +96,7 @@ instance (DecEq a, DecEq b) => DecEq (Either a b) where
 -- Fin
 --------------------------------------------------------------------------------
 
-total FZNotFS : {f : Fin n} -> FZ {k = n} = FS f -> _|_
+total FZNotFS : {f : Fin n} -> FZ {k = n} = FS f -> Void
 FZNotFS Refl impossible
 
 instance DecEq (Fin n) where
@@ -111,16 +111,16 @@ instance DecEq (Fin n) where
 -- Tuple
 --------------------------------------------------------------------------------
 
-lemma_both_neq : {x : a, y : b, x' : c, y' : d} -> (x = x' -> _|_) -> (y = y' -> _|_) -> ((x, y) = (x', y') -> _|_)
+lemma_both_neq : {x : a, y : b, x' : c, y' : d} -> (x = x' -> Void) -> (y = y' -> Void) -> ((x, y) = (x', y') -> Void)
 lemma_both_neq p_x_not_x' p_y_not_y' Refl = p_x_not_x' Refl
 
-lemma_snd_neq : {x : a, y : b, y' : d} -> (x = x) -> (y = y' -> _|_) -> ((x, y) = (x, y') -> _|_)
+lemma_snd_neq : {x : a, y : b, y' : d} -> (x = x) -> (y = y' -> Void) -> ((x, y) = (x, y') -> Void)
 lemma_snd_neq Refl p Refl = p Refl
 
 lemma_fst_neq_snd_eq : {x : a, x' : b, y : c, y' : d} ->
-                       (x = x' -> _|_) ->
+                       (x = x' -> Void) ->
                        (y = y') ->
-                       ((x, y) = (x', y) -> _|_)
+                       ((x, y) = (x', y) -> Void)
 lemma_fst_neq_snd_eq p_x_not_x' Refl Refl = p_x_not_x' Refl
 
 instance (DecEq a, DecEq b) => DecEq (a, b) where
@@ -137,16 +137,16 @@ instance (DecEq a, DecEq b) => DecEq (a, b) where
 -- List
 --------------------------------------------------------------------------------
 
-lemma_val_not_nil : {x : t, xs : List t} -> ((x :: xs) = Prelude.List.Nil {a = t} -> _|_)
+lemma_val_not_nil : {x : t, xs : List t} -> ((x :: xs) = Prelude.List.Nil {a = t} -> Void)
 lemma_val_not_nil Refl impossible
 
-lemma_x_eq_xs_neq : {x : t, xs : List t, y : t, ys : List t} -> (x = y) -> (xs = ys -> _|_) -> ((x :: xs) = (y :: ys) -> _|_)
+lemma_x_eq_xs_neq : {x : t, xs : List t, y : t, ys : List t} -> (x = y) -> (xs = ys -> Void) -> ((x :: xs) = (y :: ys) -> Void)
 lemma_x_eq_xs_neq Refl p Refl = p Refl
 
-lemma_x_neq_xs_eq : {x : t, xs : List t, y : t, ys : List t} -> (x = y -> _|_) -> (xs = ys) -> ((x :: xs) = (y :: ys) -> _|_)
+lemma_x_neq_xs_eq : {x : t, xs : List t, y : t, ys : List t} -> (x = y -> Void) -> (xs = ys) -> ((x :: xs) = (y :: ys) -> Void)
 lemma_x_neq_xs_eq p Refl Refl = p Refl
 
-lemma_x_neq_xs_neq : {x : t, xs : List t, y : t, ys : List t} -> (x = y -> _|_) -> (xs = ys -> _|_) -> ((x :: xs) = (y :: ys) -> _|_)
+lemma_x_neq_xs_neq : {x : t, xs : List t, y : t, ys : List t} -> (x = y -> Void) -> (xs = ys -> Void) -> ((x :: xs) = (y :: ys) -> Void)
 lemma_x_neq_xs_neq p p' Refl = p Refl
 
 instance DecEq a => DecEq (List a) where
@@ -203,7 +203,7 @@ instance DecEq Int where
     decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
        where primitiveEq : x = y
              primitiveEq = believe_me (Refl {x})
-             postulate primitiveNotEq : x = y -> _|_
+             postulate primitiveNotEq : x = y -> Void
 
 --------------------------------------------------------------------------------
 -- Char
@@ -213,7 +213,7 @@ instance DecEq Char where
     decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
        where primitiveEq : x = y
              primitiveEq = believe_me (Refl {x})
-             postulate primitiveNotEq : x = y -> _|_
+             postulate primitiveNotEq : x = y -> Void
 
 --------------------------------------------------------------------------------
 -- Integer
@@ -223,7 +223,7 @@ instance DecEq Integer where
     decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
        where primitiveEq : x = y
              primitiveEq = believe_me (Refl {x})
-             postulate primitiveNotEq : x = y -> _|_
+             postulate primitiveNotEq : x = y -> Void
 
 --------------------------------------------------------------------------------
 -- Float
@@ -233,7 +233,7 @@ instance DecEq Float where
     decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
        where primitiveEq : x = y
              primitiveEq = believe_me (Refl {x})
-             postulate primitiveNotEq : x = y -> _|_
+             postulate primitiveNotEq : x = y -> Void
 
 --------------------------------------------------------------------------------
 -- String
@@ -243,6 +243,6 @@ instance DecEq String where
     decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
        where primitiveEq : x = y
              primitiveEq = believe_me (Refl {x})
-             postulate primitiveNotEq : x = y -> _|_
+             postulate primitiveNotEq : x = y -> Void
 
 

libs/prelude/Prelude/Basics.idr

@@ -3,7 +3,7 @@ module Prelude.Basics
 import Builtins
 
 Not : Type -> Type
-Not a = a -> _|_
+Not a = a -> Void
 
 ||| Identity function.
 id : a -> a
@@ -55,5 +55,5 @@ data Dec : Type -> Type where
 
   ||| The case where the property holding would be a contradiction
   ||| @ contra a demonstration that A would be a contradiction
-  No  : {A : Type} -> (contra : A -> _|_) -> Dec A
+  No  : {A : Type} -> (contra : A -> Void) -> Dec A
 

libs/prelude/Prelude/Fin.idr

@@ -28,11 +28,11 @@ instance Eq (Fin n) where
     (==) _ _ = False
 
 ||| There are no elements of `Fin Z`
-FinZAbsurd : Fin Z -> _|_
+FinZAbsurd : Fin Z -> Void
 FinZAbsurd FZ impossible
 
 FinZElim : Fin Z -> a
-FinZElim x = FalseElim (FinZAbsurd x)
+FinZElim x = void (FinZAbsurd x)
 
 ||| Convert a Fin to a Nat
 finToNat : Fin n -> Nat