mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 12:42:02 +03:00
f078d5f5dc
* deprecate Data.Nat.Order.decideLTE * Add properties for LTE/GTE that produce the difference. * remove deprecated function now that it is available in the base library. * remove two deprecated lines. * remove module deprecated since v0.4.0 * fix prelude reference to renamed primitive. * finish removing Data.Num.Implementations * remove deprecated dirEntry function. * remove deprecated fastAppend. Update CHANGELOG. * replace fastAppend in test case * replace fastAppend uses in compiler. * remove new properties that weren't actually very new.
43 lines
880 B
Idris
43 lines
880 B
Idris
module Prelude.Uninhabited
|
|
|
|
import Builtin
|
|
import Prelude.Basics
|
|
|
|
%default total
|
|
|
|
||| A canonical proof that some type is empty.
|
|
public export
|
|
interface Uninhabited t where
|
|
constructor MkUninhabited
|
|
||| If I have a t, I've had a contradiction.
|
|
||| @ t the uninhabited type
|
|
uninhabited : t -> Void
|
|
|
|
%extern
|
|
prim__void : (0 x : Void) -> a
|
|
|
|
||| The eliminator for the `Void` type.
|
|
public export
|
|
void : (0 x : Void) -> a
|
|
void = prim__void
|
|
|
|
export
|
|
Uninhabited Void where
|
|
uninhabited = id
|
|
|
|
||| Use an absurd assumption to discharge a proof obligation.
|
|
||| @ t some empty type
|
|
||| @ a the goal type
|
|
||| @ h the contradictory hypothesis
|
|
public export
|
|
absurd : Uninhabited t => (h : t) -> a
|
|
absurd h = void (uninhabited h)
|
|
|
|
public export
|
|
Uninhabited (True = False) where
|
|
uninhabited Refl impossible
|
|
|
|
public export
|
|
Uninhabited (False = True) where
|
|
uninhabited Refl impossible
|