git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1619 from ahmadsalim/feature/renamevoid

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

commite890280366f9a61fbfa55d4bc7aae7d008395a08 authorEdwin Brady <edwin.brady@gmail.com> dateTue 14 Oct 2014, 11:22 (12 years ago) parent7a0f64dd6981dc
38 files changed+108−132
compare with master
unifiedsplit
benchmarks/quasigroups/Solver.idr+2−2 libs/base/Control/Isomorphism.idr+21−21 libs/base/Data/Heap.idr+3−3 libs/base/Data/List.idr+2−2 libs/base/Data/Vect.idr+1−1 libs/base/Data/Vect/Quantifiers.idr+3−3 libs/base/Data/ZZ.idr+1−1 libs/base/Decidable/Order.idr+3−3 libs/prelude/Builtins.idr+8−2 libs/prelude/Decidable/Equality.idr+19−19 libs/prelude/Prelude/Basics.idr+2−2 libs/prelude/Prelude/Fin.idr+2−2 libs/prelude/Prelude/Uninhabited.idr+3−3 src/Idris/AbsSyntax.hs−2 src/Idris/AbsSyntaxTree.hs+5−11 src/Idris/Apropos.hs−1 src/Idris/DeepSeq.hs−1 src/Idris/Delaborate.hs−1 src/Idris/Docs.hs−2 src/Idris/ElabDecls.hs+4−4 src/Idris/ElabTerm.hs−1 src/Idris/Erasure.hs−3 src/Idris/Error.hs−1 src/Idris/IBC.hs−4 src/Idris/ParseExpr.hs+2−5 src/Idris/REPLParser.hs+1−6 test/ffi005/Postulate.idr+1−1 test/proof005/DefaultArgSubstitutionSuccess.idr+3−3 test/proof006/DefaultArgSubstitutionSyntax.idr+2−2 test/quasiquote001/expected+3−3 test/reg002/reg002.idr+4−4 test/reg012/reg012.lidr+2−2 test/reg035/reg035b.idr+1−1 test/reg041/ott.idr+1−1 test/reg049/expected+1−1 test/reg049/reg049.idr+2−2 test/totality002/test017b.idr+1−1 test/tutorial004/tutorial004.idr+5−5
benchmarks/quasigroups/Solver.idr+2−2
@@ -103,8 +103,8 @@ legalVal b (x, y) v =
103103Filled : Cell n -> Type
104104--Filled {n=n} x = Not (Empty x) -- TODO: Find out why this doesn't work
105105Filled {n=n} = (\x => Not (Empty x))
106−--Filled {n=n} x = the (Maybe (Fin n)) Nothing = x -> _|_
107−--Filled {n=n} = \x => the (Maybe (Fin n)) Nothing = x -> _|_
106+--Filled {n=n} x = the (Maybe (Fin n)) Nothing = x -> Void
107+--Filled {n=n} = \x => the (Maybe (Fin n)) Nothing = x -> Void
108108
109109filled : (cell : Cell n) -> Dec (Filled cell)
110110filled Nothing = No (\f => f Refl)
libs/base/Control/Isomorphism.idr+21−21
@@ -70,21 +70,21 @@ eitherAssoc = MkIso eitherAssoc1 eitherAssoc2 ok1 ok2
7070 ok2 (Right x) = Refl
7171
7272||| Disjunction with false is a no-op
73−eitherBotLeft : Iso (Either _|_ a) a
73+eitherBotLeft : Iso (Either Void a) a
7474eitherBotLeft = MkIso to from ok1 ok2
75− where to : Either _|_ a -> a
76− to (Left x) = FalseElim x
75+ where to : Either Void a -> a
76+ to (Left x) = void x
7777 to (Right x) = x
78− from : a -> Either _|_ a
78+ from : a -> Either Void a
7979 from = Right
8080 ok1 : (x : a) -> to (from x) = x
8181 ok1 x = Refl
82− ok2 : (x : Either _|_ a) -> from (to x) = x
83− ok2 (Left x) = FalseElim x
82+ ok2 : (x : Either Void a) -> from (to x) = x
83+ ok2 (Left x) = void x
8484 ok2 (Right x) = Refl
8585
8686||| Disjunction with false is a no-op
87−eitherBotRight : Iso (Either a _|_) a
87+eitherBotRight : Iso (Either a Void) a
8888eitherBotRight = isoTrans eitherComm eitherBotLeft
8989
9090||| Isomorphism is a congruence with regards to disjunction
@@ -145,11 +145,11 @@ pairUnitLeft : Iso ((), a) a
145145pairUnitLeft = isoTrans pairComm pairUnitRight
146146
147147||| Conjunction preserves falsehood
148−pairBotLeft : Iso (_|_, a) _|_
149−pairBotLeft = MkIso fst FalseElim (\x => FalseElim x) (\y => FalseElim (fst y))
148+pairBotLeft : Iso (Void, a) Void
149+pairBotLeft = MkIso fst void (\x => void x) (\y => void (fst y))
150150
151151||| Conjunction preserves falsehood
152−pairBotRight : Iso (a, _|_) _|_
152+pairBotRight : Iso (a, Void) Void
153153pairBotRight = isoTrans pairComm pairBotLeft
154154
155155||| Isomorphism is a congruence with regards to conjunction
@@ -240,9 +240,9 @@ maybeEither = MkIso to from iso1 iso2
240240 iso2 (Just x) = Refl
241241
242242||| Maybe of void is just unit
243−maybeVoidUnit : Iso (Maybe _|_) ()
244−maybeVoidUnit = (Maybe _|_) ={ maybeEither }=
245− (Either _|_ ()) ={ eitherBotLeft }=
243+maybeVoidUnit : Iso (Maybe Void) ()
244+maybeVoidUnit = (Maybe Void) ={ maybeEither }=
245+ (Either Void ()) ={ eitherBotLeft }=
246246 () QED
247247
248248eitherMaybeLeftMaybe : Iso (Either (Maybe a) b) (Maybe (Either a b))
@@ -280,16 +280,16 @@ maybeIsoS = MkIso forth back fb bf
280280 fb FZ = Refl
281281 fb (FS x) = Refl
282282
283−finZeroBot : Iso (Fin 0) _|_
284−finZeroBot = MkIso (\x => FalseElim (uninhabited x))
285− (\x => FalseElim x)
286− (\x => FalseElim x)
287− (\x => FalseElim (uninhabited x))
283+finZeroBot : Iso (Fin 0) Void
284+finZeroBot = MkIso (\x => void (uninhabited x))
285+ (\x => void x)
286+ (\x => void x)
287+ (\x => void (uninhabited x))
288288
289289eitherFinPlus : Iso (Either (Fin m) (Fin n)) (Fin (m + n))
290290eitherFinPlus {m = Z} {n=n} =
291291 (Either (Fin 0) (Fin n)) ={ eitherCongLeft finZeroBot }=
292− (Either _|_ (Fin n)) ={ eitherBotLeft }=
292+ (Either Void (Fin n)) ={ eitherBotLeft }=
293293 (Fin n) QED
294294eitherFinPlus {m = S k} {n=n} =
295295 (Either (Fin (S k)) (Fin n)) ={ eitherCongLeft (isoSym maybeIsoS) }=
@@ -302,8 +302,8 @@ eitherFinPlus {m = S k} {n=n} =
302302finPairTimes : Iso (Fin m, Fin n) (Fin (m * n))
303303finPairTimes {m = Z} {n=n} =
304304 (Fin Z, Fin n) ={ pairCongLeft finZeroBot }=
305− (_|_, Fin n) ={ pairBotLeft }=
306− _|_ ={ isoSym finZeroBot }=
305+ (Void, Fin n) ={ pairBotLeft }=
306+ Void ={ isoSym finZeroBot }=
307307 (Fin Z) QED
308308finPairTimes {m = S k} {n=n} =
309309 (Fin (S k), Fin n) ={ pairCongLeft (isoSym maybeIsoS) }=
libs/base/Data/Heap.idr+3−3
@@ -135,12 +135,12 @@ instance Ord a => JoinSemilattice (MaxiphobicHeap a) where
135135-- Properties
136136--------------------------------------------------------------------------------
137137
138−total absurdBoolDischarge : False = True -> _|_
138+total absurdBoolDischarge : False = True -> Void
139139absurdBoolDischarge p = replace {P = disjointTy} p ()
140140 where
141141 total disjointTy : Bool -> Type
142142 disjointTy False = ()
143− disjointTy True = _|_
143+ disjointTy True = Void
144144
145145total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z
146146isEmptySizeZero Empty p = Refl
@@ -169,7 +169,7 @@ mergePreservesValidHeaps (Node ls ll le lr) (Node rs rl re rr) lp rp =
169169
170170isEmptySizeZeroNodeAbsurd = proof {
171171 intros;
172− refine FalseElim;
172+ refine void;
173173 refine absurdBoolDischarge;
174174 exact p;
175175}
libs/base/Data/List.idr+2−2
@@ -32,7 +32,7 @@ isElem x (y :: xs) with (decEq x y)
3232 isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)
3333 where
3434 mkNo : {xs' : List a} ->
35− ((x' = y') -> _|_) -> (Elem x' xs' -> _|_) ->
36− Elem x' (y' :: xs') -> _|_
35+ ((x' = y') -> Void) -> (Elem x' xs' -> Void) ->
36+ Elem x' (y' :: xs') -> Void
3737 mkNo f g Here = f Refl
3838 mkNo f g (There x) = g x
libs/base/Data/Vect.idr+1−1
@@ -15,7 +15,7 @@ data Elem : a -> Vect k a -> Type where
1515 There : Elem x xs -> Elem x (y::xs)
1616
1717||| Nothing can be in an empty Vect
18−noEmptyElem : {x : a} -> Elem x [] -> _|_
18+noEmptyElem : {x : a} -> Elem x [] -> Void
1919noEmptyElem Here impossible
2020
2121||| An item not in the head and not in the tail is not in the Vect at all
libs/base/Data/Vect/Quantifiers.idr+3−3
@@ -10,7 +10,7 @@ data Any : (P : a -> Type) -> Vect n a -> Type where
1010 There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)
1111
1212||| No element of an empty vector satisfies any property
13−anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_
13+anyNilAbsurd : {P : a -> Type} -> Any P Nil -> Void
1414anyNilAbsurd (Here _) impossible
1515anyNilAbsurd (There _) impossible
1616
@@ -48,11 +48,11 @@ negAnyAll : {P : a -> Type} -> {xs : Vect n a} -> Not (Any P xs) -> All (\x => N
4848negAnyAll {xs=Nil} _ = Nil
4949negAnyAll {xs=(x::xs)} f = (\x => f (Here x)) :: negAnyAll (\x => f (There x))
5050
51−notAllHere : {P : a -> Type} -> {xs : Vect n a} -> Not (P x) -> All P (x :: xs) -> _|_
51+notAllHere : {P : a -> Type} -> {xs : Vect n a} -> Not (P x) -> All P (x :: xs) -> Void
5252notAllHere _ Nil impossible
5353notAllHere np (p :: _) = np p
5454
55−notAllThere : {P : a -> Type} -> {xs : Vect n a} -> Not (All P xs) -> All P (x :: xs) -> _|_
55+notAllThere : {P : a -> Type} -> {xs : Vect n a} -> Not (All P xs) -> All P (x :: xs) -> Void
5656notAllThere _ Nil impossible
5757notAllThere np (_ :: ps) = np ps
5858
libs/base/Data/ZZ.idr+1−1
@@ -122,7 +122,7 @@ posInjective Refl = Refl
122122negSInjective : NegS n = NegS m -> n = m
123123negSInjective Refl = Refl
124124
125−posNotNeg : Pos n = NegS m -> _|_
125+posNotNeg : Pos n = NegS m -> Void
126126posNotNeg Refl impossible
127127
128128-- Decidable equality
libs/base/Decidable/Order.idr+3−3
@@ -84,15 +84,15 @@ LTEIsAntisymmetric (S n) (S m) (LTESucc mLTEn) (LTESucc nLTEm) with (LTEIsAntisy
8484instance Poset Nat LTE where
8585 antisymmetric = LTEIsAntisymmetric
8686
87−total zeroNeverGreater : {n : Nat} -> LTE (S n) Z -> _|_
87+total zeroNeverGreater : {n : Nat} -> LTE (S n) Z -> Void
8888zeroNeverGreater {n} LTEZero impossible
8989zeroNeverGreater {n} (LTESucc _) impossible
9090
9191total zeroAlwaysSmaller : {n : Nat} -> LTE Z n
9292zeroAlwaysSmaller = LTEZero
9393
94−total ltesuccinjective : {n : Nat} -> {m : Nat} -> (LTE n m -> _|_) -> LTE (S n) (S m) -> _|_
95−ltesuccinjective {n} {m} disprf (LTESucc nLTEm) = FalseElim (disprf nLTEm)
94+total ltesuccinjective : {n : Nat} -> {m : Nat} -> (LTE n m -> Void) -> LTE (S n) (S m) -> Void
95+ltesuccinjective {n} {m} disprf (LTESucc nLTEm) = void (disprf nLTEm)
9696ltesuccinjective {n} {m} disprf LTEZero impossible
9797
9898
libs/prelude/Builtins.idr+8−2
@@ -29,8 +29,14 @@ data Pair : (A : Type) -> (B : Type) -> Type where
2929data Sigma : (a : Type) -> (P : a -> Type) -> Type where
3030 MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P
3131
32−||| The eliminator for the empty type.
33−FalseElim : _|_ -> a
32+||| The empty type, also known as the trivially false proposition.
33+|||
34+||| Use `void` or `absurd` to prove anything if you have a variable of type `Void` in scope.
35+%elim data Void : Type where
36+
37+||| The eliminator for the `Void` type.
38+void : Void -> a
39+void {a} v = elim_for Void (\_ => a) v
3440
3541||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
3642data Symbol_ : String -> Type where
libs/prelude/Decidable/Equality.idr+19−19
@@ -13,7 +13,7 @@ import Prelude.Maybe
1313--------------------------------------------------------------------------------
1414
1515||| The negation of equality is symmetric (follows from symmetry of equality)
16−total negEqSym : {a : t} -> {b : t} -> (a = b -> _|_) -> (b = a -> _|_)
16+total negEqSym : {a : t} -> {b : t} -> (a = b -> Void) -> (b = a -> Void)
1717negEqSym p h = p (sym h)
1818
1919
@@ -36,7 +36,7 @@ instance DecEq () where
3636--------------------------------------------------------------------------------
3737-- Booleans
3838--------------------------------------------------------------------------------
39−total trueNotFalse : True = False -> _|_
39+total trueNotFalse : True = False -> Void
4040trueNotFalse Refl impossible
4141
4242instance DecEq Bool where
@@ -49,7 +49,7 @@ instance DecEq Bool where
4949-- Nat
5050--------------------------------------------------------------------------------
5151
52−total OnotS : Z = S n -> _|_
52+total OnotS : Z = S n -> Void
5353OnotS Refl impossible
5454
5555instance DecEq Nat where
@@ -64,7 +64,7 @@ instance DecEq Nat where
6464-- Maybe
6565--------------------------------------------------------------------------------
6666
67−total nothingNotJust : {x : t} -> (Nothing {a = t} = Just x) -> _|_
67+total nothingNotJust : {x : t} -> (Nothing {a = t} = Just x) -> Void
6868nothingNotJust Refl impossible
6969
7070instance (DecEq t) => DecEq (Maybe t) where
@@ -79,7 +79,7 @@ instance (DecEq t) => DecEq (Maybe t) where
7979-- Either
8080--------------------------------------------------------------------------------
8181
82−total leftNotRight : {x : a} -> {y : b} -> Left {b = b} x = Right {a = a} y -> _|_
82+total leftNotRight : {x : a} -> {y : b} -> Left {b = b} x = Right {a = a} y -> Void
8383leftNotRight Refl impossible
8484
8585instance (DecEq a, DecEq b) => DecEq (Either a b) where
@@ -96,7 +96,7 @@ instance (DecEq a, DecEq b) => DecEq (Either a b) where
9696-- Fin
9797--------------------------------------------------------------------------------
9898
99−total FZNotFS : {f : Fin n} -> FZ {k = n} = FS f -> _|_
99+total FZNotFS : {f : Fin n} -> FZ {k = n} = FS f -> Void
100100FZNotFS Refl impossible
101101
102102instance DecEq (Fin n) where
@@ -111,16 +111,16 @@ instance DecEq (Fin n) where
111111-- Tuple
112112--------------------------------------------------------------------------------
113113
114−lemma_both_neq : {x : a, y : b, x' : c, y' : d} -> (x = x' -> _|_) -> (y = y' -> _|_) -> ((x, y) = (x', y') -> _|_)
114+lemma_both_neq : {x : a, y : b, x' : c, y' : d} -> (x = x' -> Void) -> (y = y' -> Void) -> ((x, y) = (x', y') -> Void)
115115lemma_both_neq p_x_not_x' p_y_not_y' Refl = p_x_not_x' Refl
116116
117−lemma_snd_neq : {x : a, y : b, y' : d} -> (x = x) -> (y = y' -> _|_) -> ((x, y) = (x, y') -> _|_)
117+lemma_snd_neq : {x : a, y : b, y' : d} -> (x = x) -> (y = y' -> Void) -> ((x, y) = (x, y') -> Void)
118118lemma_snd_neq Refl p Refl = p Refl
119119
120120lemma_fst_neq_snd_eq : {x : a, x' : b, y : c, y' : d} ->
121− (x = x' -> _|_) ->
121+ (x = x' -> Void) ->
122122 (y = y') ->
123− ((x, y) = (x', y) -> _|_)
123+ ((x, y) = (x', y) -> Void)
124124lemma_fst_neq_snd_eq p_x_not_x' Refl Refl = p_x_not_x' Refl
125125
126126instance (DecEq a, DecEq b) => DecEq (a, b) where
@@ -137,16 +137,16 @@ instance (DecEq a, DecEq b) => DecEq (a, b) where
137137-- List
138138--------------------------------------------------------------------------------
139139
140−lemma_val_not_nil : {x : t, xs : List t} -> ((x :: xs) = Prelude.List.Nil {a = t} -> _|_)
140+lemma_val_not_nil : {x : t, xs : List t} -> ((x :: xs) = Prelude.List.Nil {a = t} -> Void)
141141lemma_val_not_nil Refl impossible
142142
143−lemma_x_eq_xs_neq : {x : t, xs : List t, y : t, ys : List t} -> (x = y) -> (xs = ys -> _|_) -> ((x :: xs) = (y :: ys) -> _|_)
143+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)
144144lemma_x_eq_xs_neq Refl p Refl = p Refl
145145
146−lemma_x_neq_xs_eq : {x : t, xs : List t, y : t, ys : List t} -> (x = y -> _|_) -> (xs = ys) -> ((x :: xs) = (y :: ys) -> _|_)
146+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)
147147lemma_x_neq_xs_eq p Refl Refl = p Refl
148148
149−lemma_x_neq_xs_neq : {x : t, xs : List t, y : t, ys : List t} -> (x = y -> _|_) -> (xs = ys -> _|_) -> ((x :: xs) = (y :: ys) -> _|_)
149+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)
150150lemma_x_neq_xs_neq p p' Refl = p Refl
151151
152152instance DecEq a => DecEq (List a) where
@@ -203,7 +203,7 @@ instance DecEq Int where
203203 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
204204 where primitiveEq : x = y
205205 primitiveEq = believe_me (Refl {x})
206− postulate primitiveNotEq : x = y -> _|_
206+ postulate primitiveNotEq : x = y -> Void
207207
208208--------------------------------------------------------------------------------
209209-- Char
@@ -213,7 +213,7 @@ instance DecEq Char where
213213 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
214214 where primitiveEq : x = y
215215 primitiveEq = believe_me (Refl {x})
216− postulate primitiveNotEq : x = y -> _|_
216+ postulate primitiveNotEq : x = y -> Void
217217
218218--------------------------------------------------------------------------------
219219-- Integer
@@ -223,7 +223,7 @@ instance DecEq Integer where
223223 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
224224 where primitiveEq : x = y
225225 primitiveEq = believe_me (Refl {x})
226− postulate primitiveNotEq : x = y -> _|_
226+ postulate primitiveNotEq : x = y -> Void
227227
228228--------------------------------------------------------------------------------
229229-- Float
@@ -233,7 +233,7 @@ instance DecEq Float where
233233 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
234234 where primitiveEq : x = y
235235 primitiveEq = believe_me (Refl {x})
236− postulate primitiveNotEq : x = y -> _|_
236+ postulate primitiveNotEq : x = y -> Void
237237
238238--------------------------------------------------------------------------------
239239-- String
@@ -243,6 +243,6 @@ instance DecEq String where
243243 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
244244 where primitiveEq : x = y
245245 primitiveEq = believe_me (Refl {x})
246− postulate primitiveNotEq : x = y -> _|_
246+ postulate primitiveNotEq : x = y -> Void
247247
248248
libs/prelude/Prelude/Basics.idr+2−2
@@ -3,7 +3,7 @@ module Prelude.Basics
33import Builtins
44
55Not : Type -> Type
6−Not a = a -> _|_
6+Not a = a -> Void
77
88||| Identity function.
99id : a -> a
@@ -55,5 +55,5 @@ data Dec : Type -> Type where
5555
5656 ||| The case where the property holding would be a contradiction
5757 ||| @ contra a demonstration that A would be a contradiction
58− No : {A : Type} -> (contra : A -> _|_) -> Dec A
58+ No : {A : Type} -> (contra : A -> Void) -> Dec A
5959
libs/prelude/Prelude/Fin.idr+2−2
@@ -28,11 +28,11 @@ instance Eq (Fin n) where
2828 (==) _ _ = False
2929
3030||| There are no elements of `Fin Z`
31−FinZAbsurd : Fin Z -> _|_
31+FinZAbsurd : Fin Z -> Void
3232FinZAbsurd FZ impossible
3333
3434FinZElim : Fin Z -> a
35−FinZElim x = FalseElim (FinZAbsurd x)
35+FinZElim x = void (FinZAbsurd x)
3636
3737||| Convert a Fin to a Nat
3838finToNat : Fin n -> Nat
libs/prelude/Prelude/Uninhabited.idr+3−3
@@ -6,9 +6,9 @@ import Builtins
66class Uninhabited t where
77 ||| If I have a t, I've had a contradiction
88 ||| @ t the uninhabited type
9− total uninhabited : t -> _|_
9+ total uninhabited : t -> Void
1010
11−instance Uninhabited _|_ where
11+instance Uninhabited Void where
1212 uninhabited a = a
1313
1414||| Use an absurd assumption to discharge a proof obligation
@@ -16,4 +16,4 @@ instance Uninhabited _|_ where
1616||| @ a the goal type
1717||| @ h the contradictory hypothesis
1818absurd : Uninhabited t => (h : t) -> a
19−absurd h = FalseElim (uninhabited h)
19+absurd h = void (uninhabited h)
src/Idris/AbsSyntax.hs−2
@@ -1040,7 +1040,6 @@ getPriority i tm = 1 -- pri tm
10401040 [] -> 0 -- must be locally bound, if it's not an error...
10411041 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
10421042 pri (PTrue _ _) = 0
1043− pri (PFalse _) = 0
10441043 pri (PRefl _ _) = 1
10451044 pri (PEq _ _ _ l r) = max 1 (max (pri l) (pri r))
10461045 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
@@ -1771,7 +1770,6 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
17711770 match (PRefl _ _) (PRefl _ _) = return []
17721771 match (PResolveTC _) (PResolveTC _) = return []
17731772 match (PTrue _ _) (PTrue _ _) = return []
1774− match (PFalse _) (PFalse _) = return []
17751773 match (PReturn _) (PReturn _) = return []
17761774 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
17771775 ms <- match' s s'
src/Idris/AbsSyntaxTree.hs+5−11
@@ -238,7 +238,7 @@ deriving instance NFData CGInfo
238238primDefs = [sUN "unsafePerformPrimIO",
239239 sUN "mkLazyForeignPrim",
240240 sUN "mkForeignPrim",
241− sUN "FalseElim"]
241+ sUN "void"]
242242
243243-- information that needs writing for the current module's .ibc file
244244data IBCWrite = IBCFix FixDecl
@@ -711,7 +711,6 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua
711711 | PMatchApp FC Name -- ^ Make an application by type matching
712712 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
713713 | PTrue FC PunInfo -- ^ Unit type..?
714− | PFalse FC -- ^ _|_
715714 | PRefl FC PTerm -- ^ The canonical proof of the equality type
716715 | PResolveTC FC -- ^ Solve this dictionary by type class resolution
717716 | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B
@@ -1074,7 +1073,7 @@ getInferType (App (App _ ty) _) = ty
10741073
10751074-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
10761075
1077−primNames = [falseTy, eqTy, eqCon, inferTy, inferCon]
1076+primNames = [eqTy, eqCon, inferTy, inferCon]
10781077
10791078unitTy = sUN "Unit"
10801079unitCon = sUN "MkUnit"
@@ -1083,11 +1082,9 @@ unitCon = sUN "MkUnit"
10831082falseDoc = fmap (const Nothing) . parseDocstring . T.pack $
10841083 "The empty type, also known as the trivially false proposition." ++
10851084 "\n\n" ++
1086− "Use `FalseElim` or `absurd` to prove anything if you have a variable " ++
1087− "of type `_|_` in scope."
1088−falseTy = sMN 0 "__False"
1089−falseDecl = PDatadecl falseTy PType []
1090−falseOpts = []
1085+ "Use `void` or `absurd` to prove anything if you have a variable " ++
1086+ "of type `Void` in scope."
1087+falseTy = sUN "Void"
10911088
10921089pairTy = sUN "Pair"
10931090pairCon = sUN "MkPair"
@@ -1323,7 +1320,6 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
13231320 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"
13241321 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
13251322 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
1326− prettySe p bnd (PFalse _) = annName falseTy $ text "_|_"
13271323 prettySe p bnd (PEq _ lt rt l r)
13281324 | ppopt_impl ppo =
13291325 bracket p 1 $
@@ -1493,7 +1489,6 @@ prettyName infixParen showNS bnd n
14931489 baseName (UN n) = T.unpack n
14941490 baseName (NS n ns) = baseName n
14951491 baseName (MN i s) = T.unpack s
1496− baseName n | n == falseTy = "_|_"
14971492 baseName other = show other
14981493 nameSpace = case n of
14991494 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
@@ -1623,7 +1618,6 @@ instance Sized PTerm where
16231618 size (PAppBind fc name args) = 1 + size args
16241619 size (PCase fc trm bdy) = 1 + size trm + size bdy
16251620 size (PTrue fc _) = 1
1626− size (PFalse fc) = 1
16271621 size (PRefl fc _) = 1
16281622 size (PResolveTC fc) = 1
16291623 size (PEq fc _ _ left right) = 1 + size left + size right
src/Idris/Apropos.hs−1
@@ -38,7 +38,6 @@ instance Apropos Name where
3838 isApropos str (NS n' ns) = isApropos str n' || any (textIn str) ns
3939 -- Handle special names from stdlib
4040 isApropos str n | (n == unitTy || n == unitCon) && str == T.pack "()" = True
41− | n == falseTy && str == T.pack "_|_" = True
4241 | (n == pairTy || n == pairCon) && str == T.pack "," = True
4342 | n == eqTy && str == T.pack "=" = True
4443 | n == eqCon && (T.toLower str) == T.pack "Refl" = True
src/Idris/DeepSeq.hs−1
@@ -202,7 +202,6 @@ instance NFData PTerm where
202202 rnf (PMatchApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
203203 rnf (PCase x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
204204 rnf (PTrue x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
205− rnf (PFalse x1) = rnf x1 `seq` ()
206205 rnf (PRefl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
207206 rnf (PResolveTC x1) = rnf x1 `seq` ()
208207 rnf (PEq x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
src/Idris/Delaborate.hs−1
@@ -50,7 +50,6 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
5050 | otherwise = PRef un (sUN ("v" ++ show i ++ ""))
5151 de env _ (P _ n _) | n == unitTy = PTrue un IsType
5252 | n == unitCon = PTrue un IsTerm
53− | n == falseTy = PFalse un
5453 | Just n' <- lookup n env = PRef un n'
5554 | otherwise
5655 = case lookup n (idris_metavars ist) of
src/Idris/Docs.hs−2
@@ -186,8 +186,6 @@ docFun n
186186 where funName :: Name -> String
187187 funName (UN n) = str n
188188 funName (NS n _) = funName n
189− funName n
190− | n == falseTy = "_|_"
191189
192190getPArgNames :: PTerm -> [(Name, Docstring (Maybe Term))] -> [(Name, PTerm, Plicity, Maybe (Docstring (Maybe Term)))]
193191getPArgNames (PPi plicity name ty body) ds =
src/Idris/ElabDecls.hs+4−4
@@ -77,10 +77,10 @@ elabPrims :: Idris ()
7777elabPrims = do mapM_ (elabDecl' EAll recinfo)
7878 (map (\(opt, decl, docs, argdocs) -> PData docs argdocs defaultSyntax (fileFC "builtin") opt decl)
7979 (zip4
80− [inferOpts, falseOpts, eqOpts]
81− [inferDecl, falseDecl, eqDecl]
82− [emptyDocstring, falseDoc, eqDoc]
83− [[], [], eqParamDoc]))
80+ [inferOpts, eqOpts]
81+ [inferDecl, eqDecl]
82+ [emptyDocstring, eqDoc]
83+ [[], eqParamDoc]))
8484 addNameHint eqTy (sUN "prf")
8585 mapM_ elabPrim primitives
8686 -- Special case prim__believe_me because it doesn't work on just constants
src/Idris/ElabTerm.hs−1
@@ -251,7 +251,6 @@ elab ist info emode opts fn tm
251251 case g of
252252 TType _ -> elab' ina (PRef fc unitTy)
253253 _ -> elab' ina (PRef fc unitCon)
254− elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)
255254 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
256255 = do g <- goal; resolveTC False 5 g fn ist
257256 elab' ina (PResolveTC fc)
src/Idris/Erasure.hs−3
@@ -342,13 +342,10 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
342342
343343 -- sanity check: machine-generated names shouldn't occur at top-level
344344 | MN _ _ <- n
345− , n `notElem` specialMNs
346345 = error $ "erasure analysis: variable " ++ show n ++ " unbound in " ++ show (S.toList cd)
347346
348347 -- assumed to be a global reference
349348 | otherwise = M.singleton cd (M.singleton (n, Result) S.empty)
350− where
351− specialMNs = [falseTy]
352349
353350 -- dependencies of de bruijn variables are described in `bs'
354351 getDepsTerm vs bs cd (V i) = snd (bs !! i) cd
src/Idris/Error.hs−1
@@ -99,7 +99,6 @@ warnDisamb ist (PMatchApp _ _) = return ()
9999warnDisamb ist (PCase _ tm cases) = warnDisamb ist tm >>
100100 mapM_ (\(x,y)-> warnDisamb ist x >> warnDisamb ist y) cases
101101warnDisamb ist (PTrue _ _) = return ()
102−warnDisamb ist (PFalse _) = return ()
103102warnDisamb ist (PRefl _ tm) = warnDisamb ist tm
104103warnDisamb ist (PResolveTC _) = return ()
105104warnDisamb ist (PEq _ a b x y) = warnDisamb ist a >> warnDisamb ist b >>
src/Idris/IBC.hs−4
@@ -1435,8 +1435,6 @@ instance Binary PTerm where
14351435 PTrue x1 x2 -> do putWord8 12
14361436 put x1
14371437 put x2
1438− PFalse x1 -> do putWord8 13
1439− put x1
14401438 PRefl x1 x2 -> do putWord8 14
14411439 put x1
14421440 put x2
@@ -1553,8 +1551,6 @@ instance Binary PTerm where
15531551 12 -> do x1 <- get
15541552 x2 <- get
15551553 return (PTrue x1 x2)
1556− 13 -> do x1 <- get
1557− return (PFalse x1)
15581554 14 -> do x1 <- get
15591555 x2 <- get
15601556 return (PRefl x1 x2)
src/Idris/ParseExpr.hs+2−5
@@ -293,7 +293,7 @@ SimpleExpr ::=
293293 | Bracketed
294294 | Constant
295295 | Type
296− | '_|_'
296+ | 'Void'
297297 | Quasiquote
298298 | Unquote
299299 | '_'
@@ -333,9 +333,6 @@ simpleExpr syn =
333333 fc <- getFC
334334 return (PAppBind fc s [])
335335 <|> bracketed (disallowImp syn)
336− <|> do symbol "_|_"
337− fc <- getFC
338− return (PFalse fc)
339336 <|> quasiquote syn
340337 <|> unquote syn
341338 <|> do lchar '_'; return Placeholder
@@ -1308,7 +1305,7 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (
13081305 return (TDocStr (Right c)))
13091306 <|> try (do reserved "doc"
13101307 whiteSpace
1311− n <- (fnName <|> (string "_|_" >> return falseTy))
1308+ n <- fnName
13121309 eof
13131310 return (TDocStr (Left n)))
13141311 <|> try (do reserved "search"
src/Idris/REPLParser.hs+1−6
@@ -208,14 +208,9 @@ cmd_doc name = do
208208 eof
209209 return $ Right (DocStr (Right c))
210210
211− let bottom = do
212− P.string "_|_"
213− eof
214− return $ Right (DocStr (Left falseTy))
215−
216211 let fnName = fnNameArg name (\n -> DocStr (Left n))
217212
218− try constant <|> try bottom <|> fnName
213+ try constant <|> fnName
219214
220215cmd_consolewidth :: String -> P.IdrisParser (Either String Command)
221216cmd_consolewidth name = do
test/ffi005/Postulate.idr+1−1
@@ -5,7 +5,7 @@ import Providers
55%language TypeProviders
66
77bad : IO (Provider Type)
8−bad = return $ pure _|_
8+bad = return $ pure Void
99
1010%provide postulate oops with bad
1111
test/proof005/DefaultArgSubstitutionSuccess.idr+3−3
@@ -2,7 +2,7 @@ module DefaultArgSubstitutionSuccess
22
33DecProofType : {a:Type} -> Dec a -> Type
44DecProofType {a} (Yes _) = a
5−DecProofType {a} (No _) = a -> _|_
5+DecProofType {a} (No _) = a -> Void
66
77decProof : {a:Type} -> (dec : Dec a) -> DecProofType dec
88decProof (Yes x) = x
@@ -18,7 +18,7 @@ argsAreSame _ _ = ()
1818
1919
2020argsAreDiff : (n:Nat) -> (m:Nat)
21− -> { default (decProof (decEq m n)) same : (m=n) -> _|_ } -> ()
21+ -> { default (decProof (decEq m n)) same : (m=n) -> Void } -> ()
2222argsAreDiff _ _ = ()
2323
2424
@@ -28,7 +28,7 @@ data SameNats : Type where
2828
2929data DiffNats : Type where
3030 diff : (n:Nat) -> (m:Nat) ->
31− { default (decProof (decEq m n)) same : (m=n) -> _|_ } -> DiffNats
31+ { default (decProof (decEq m n)) same : (m=n) -> Void } -> DiffNats
3232
3333
3434zArgsAreSame : ()
test/proof006/DefaultArgSubstitutionSyntax.idr+2−2
@@ -2,7 +2,7 @@ module DefaultArgSubstitutionSyntax
22
33DecProofType : {a:Type} -> Dec a -> Type
44DecProofType {a} (Yes _) = a
5−DecProofType {a} (No _) = a -> _|_
5+DecProofType {a} (No _) = a -> Void
66
77decProof : {a:Type} -> (dec : Dec a) -> DecProofType dec
88decProof (Yes x) = x
@@ -16,7 +16,7 @@ syntax "{{" [prfname] ":" "accept" [dec] "}}" "->" [ret]
1616 = { default (decProof dec) prfname : DecType dec } -> ret
1717
1818syntax "{{" [prfname] ":" "reject" [dec] "}}" "->" [ret]
19− = { default (decProof dec) prfname : DecType dec -> _|_ } -> ret
19+ = { default (decProof dec) prfname : DecType dec -> Void } -> ret
2020
2121
2222argsAreSame : (n:Nat) -> (m:Nat)
test/quasiquote001/expected+3−3
@@ -1,5 +1,5 @@
1−(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 9 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 9 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 9 0) (UN Unit) (TType (UVar -1))))))
1+(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN Unit) (TType (UVar -1))))))
22--------------
3−(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 50))) (TType (UVar 52))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 54))) (App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 44))) (TType (UVar 46))) (P (TCon 9 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 9 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 56)))))
3+(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 48))) (TType (UVar 50))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 52))) (App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 54)))))
44--------------
5−(App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 44))) (TType (UVar 46))) (App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 44))) (TType (UVar 46))) (TType (UVar 50))) (TType (UVar 50)))) (App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 44))) (TType (UVar 46))) (TType (UVar 50))) (TType (UVar 50))))
5+(App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (TType (UVar 48))) (TType (UVar 48)))) (App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (TType (UVar 48))) (TType (UVar 48))))
test/reg002/reg002.idr+4−4
@@ -10,16 +10,16 @@ S : CoNat -> CoNat
1010S (Co n) = Co (S n)
1111S Infinity = Infinity
1212
13−Sn_notzero : Main.S n = Co 0 -> _|_
13+Sn_notzero : Main.S n = Co 0 -> Void
1414Sn_notzero = believe_me
1515
16−S_Co_not_Inf : Main.S (Co n) = Infinity -> _|_
16+S_Co_not_Inf : Main.S (Co n) = Infinity -> Void
1717S_Co_not_Inf = believe_me
1818
1919S_inj : (n : CoNat) -> (m : CoNat) -> Main.S n = Main.S m -> n = m
2020S_inj (Co n) (Co _) Refl = Refl
21−S_inj (Co n) Infinity p = FalseElim (S_Co_not_Inf p)
22−S_inj Infinity (Co m) p = FalseElim (S_Co_not_Inf (sym p))
21+S_inj (Co n) Infinity p = void (S_Co_not_Inf p)
22+S_inj Infinity (Co m) p = void (S_Co_not_Inf (sym p))
2323S_inj Infinity Infinity Refl = Refl
2424
2525swap : {n : Nat} -> Vect n a -> Vect n a
test/reg012/reg012.lidr+2−2
@@ -4,11 +4,11 @@
44> soElim C coh .True .Oh = coh
55
66> soFalseElim : So False -> a
7−> soFalseElim x = FalseElim (soElim C () False x)
7+> soFalseElim x = void (soElim C () False x)
88> where
99> C : (b : Bool) -> So b -> Type
1010> C True s = ()
11−> C False s = _|_
11+> C False s = Void
1212
1313> soTrue : So b -> b = True
1414> soTrue {b = False} x = soFalseElim x
test/reg035/reg035b.idr+1−1
@@ -6,6 +6,6 @@ finZEmpty : Fin Z -> a
66fins : (n : Nat) -> (xs : Vect n (Fin n) ** ((x : Fin n) -> Elem x xs))
77fins Z = ([] ** (finZEmpty {a=_}))
88
9−-- f : (a : Nat) -> a = S a -> _|_
9+-- f : (a : Nat) -> a = S a -> Void
1010-- f a = believe_me
1111
test/reg041/ott.idr+1−1
@@ -11,7 +11,7 @@ mutual
1111
1212 El : U -> Type
1313 El u = U
14− El zero = _|_
14+ El zero = Void
1515 El one = ()
1616 El two = Bool
1717 El (pi s t) = (x : El s) -> El (t x)
test/reg049/expected+1−1
@@ -1,2 +1,2 @@
11reg049.idr:2:9:When elaborating constructor Main.Bogus:
2−{__False0} is not Main.Foo
2+Void is not Main.Foo
test/reg049/reg049.idr+2−2
@@ -1,5 +1,5 @@
11data Foo : Type where
2− Bogus : _|_
2+ Bogus : Void
33
4−uhOh : _|_
4+uhOh : Void
55uhOh = Bogus
test/totality002/test017b.idr+1−1
@@ -1,5 +1,5 @@
11module foo
22
3−total foo : _|_
3+total foo : Void
44foo = foo
55
test/tutorial004/tutorial004.idr+5−5
@@ -5,23 +5,23 @@ fiveIsFive = Refl
55twoPlusTwo : 2 + 2 = 4
66twoPlusTwo = Refl
77
8−total disjoint : (n : Nat) -> Z = S n -> _|_
8+total disjoint : (n : Nat) -> Z = S n -> Void
99disjoint n p = replace {P = disjointTy} p ()
1010 where
1111 disjointTy : Nat -> Type
1212 disjointTy Z = ()
13− disjointTy (S k) = _|_
13+ disjointTy (S k) = Void
1414
15−total acyclic : (n : Nat) -> n = S n -> _|_
15+total acyclic : (n : Nat) -> n = S n -> Void
1616acyclic Z p = disjoint _ p
1717acyclic (S k) p = acyclic k (succInjective _ _ p)
1818
19−empty1 : _|_
19+empty1 : Void
2020empty1 = hd [] where
2121 hd : List a -> a
2222 hd (x :: xs) = x
2323
24−empty2 : _|_
24+empty2 : Void
2525empty2 = empty2
2626
2727plusReduces : (n:Nat) -> plus Z n = n