strictRefl : a = b -> Lazy c -> c
Pattern-match on an equality proof so that the second argument to
strictRefl is only returned once the first is canonical.
Totality: total
Visibility: exportdata LT : Int -> Int -> Type
`LT a b` is a proof that `a` is less than `b` which is to say that
the function call `a < b` returns `True`.
NB: we do not re-export the constructor so that users cannot force
our magic functions to blow up in absurd contexts by bypassing the
safety measures introduced by the `strictX` functions.
We do provide functions corresponding to the wrapping and unwrapping
of `LT` but, crucially, they do not let people force `LT` proofs to
be in canonical form.
Totality: total
Visibility: export
Constructor: MkLT : a < b = True -> LT a b
mkLT : a < b = True -> LT a b
We may prove `LT a b` by using a proof that `a < b` returns `True`.
Totality: total
Visibility: exportrunLT : LT a b -> a < b = True
From a proof that `LT a b`, we may concluded that `a < b` returns `True`.
Totality: total
Visibility: exportstrictLT : LT a b -> Lazy c -> c
Do not trust arbitrary `LT` proofs when manufacturing magic ones:
be strict!
Totality: total
Visibility: exportdecide : (a : Int) -> (b : Int) -> Dec (LT a b)
LT is decidable, by virtue of being the reflection of a boolean function
Totality: total
Visibility: exporttrans : LT a b -> LT b c -> LT a (the Int c)
LT is a transitive relation. This cannot be proven so we use a magic trick.
Totality: total
Visibility: exportirrefl : Not (LT a a)
LT is an irreflexive relation.
The crash will never happen because the `LT a a` argument will never reduce
to a canonical form (unless the built-in function (<) is buggy).
Totality: total
Visibility: exportGT : Int -> Int -> Type
GT is defined in terms of LT to avoid code duplication
Totality: total
Visibility: public exportLT_not_GT : LT a b -> Not (GT a b)
- Totality: total
Visibility: export GT_not_LT : GT a b -> Not (LT a b)
- Totality: total
Visibility: export data EQ : Int -> Int -> Type
`EQ a b` is a proof that `a` is equal to `b` which is to say that
the function call `a == b` returns `True`.
NB: we do not re-export the constructor so that users cannot force
our magic functions to blow up in absurd contexts by bypassing the
safety measures introduced by the `strictX` functions.
We do provide functions corresponding to the wrapping and unwrapping
of `EQ` but, crucially, they do not let people force `EQ` proofs to
be in canonical form.
Totality: total
Visibility: export
Constructor: MkEQ : a == b = True -> EQ a b
mkEQ : a == b = True -> EQ a b
We may prove `EQ a b` by using a proof that `a == b` returns `True`.
Totality: total
Visibility: exportrunEQ : EQ a b -> a == b = True
From a proof that `EQ a b`, we may concluded that `a == b` returns `True`.
Totality: total
Visibility: exportstrictEQ : EQ a b -> Lazy c -> c
Do not trust arbitrary `EQ` proofs when manufacturing magic ones:
be strict!
Totality: total
Visibility: exportdecide : (a : Int) -> (b : Int) -> Dec (EQ a b)
EQ is decidable, by virtue of being the reflection of a boolean function
Totality: total
Visibility: exportrefl : EQ a a
EQ is a reflexive relation
Totality: total
Visibility: exportelimEQ : (0 p : (Int -> Type)) -> EQ a b -> p a -> p b
EQ is substitutive
Totality: total
Visibility: exportreflect : EQ a b -> a = b
EQ implies propositional equality
Totality: total
Visibility: exportsym : EQ a b -> EQ b a
EQ is a symmetric relation
Totality: total
Visibility: exporttrans : EQ a b -> EQ b c -> EQ a c
EQ is a transitive relation
Totality: total
Visibility: exporttrans_LT_EQ : LT a b -> EQ b c -> LT a c
- Totality: total
Visibility: export trans_EQ_LT : EQ a b -> LT b c -> LT a c
- Totality: total
Visibility: export LT_not_EQ : LT a b -> Not (EQ a b)
- Totality: total
Visibility: export EQ_not_LT : EQ a b -> Not (LT a b)
- Totality: total
Visibility: export EQ_not_GT : EQ a b -> Not (GT a b)
- Totality: total
Visibility: export GT_not_EQ : GT a b -> Not (EQ a b)
- Totality: total
Visibility: export data LTE : Int -> Int -> Type
`LTE a b` is a proof that `a` is less or equal to `b` which is to say that
the function call `a < b` or `a == b` returns `True`.
NB: we do not re-export the constructor so that users cannot force
our magic functions to blow up in absurd contexts by bypassing the
safety measures introduced by the `strictX` functions.
Totality: total
Visibility: export
Constructors:
MkLT : a < b = True -> LTE a b
MkEQ : a == b = True -> LTE a b
runLTE : LTE a b -> Either (LT a b) (EQ a b)
Unwrap an LTE proof to get either an LT or an EQ one
Totality: total
Visibility: exportstrictLTE : LTE a b -> Lazy c -> c
Do not trust arbitrary `LTE` proofs when manufacturing magic ones:
be strict!
Totality: total
Visibility: exportdecide : (a : Int) -> (b : Int) -> Dec (LTE a b)
LTE is decidable by virture of both LT and EQ being decidable
Totality: total
Visibility: exportrefl : LTE a a
LTE is a reflexive relation
Totality: total
Visibility: exporttrans_LT_LTE : LT a b -> LTE b c -> LT a c
- Totality: total
Visibility: export trans_LTE_LT : LTE a b -> LT b c -> LT a c
- Totality: total
Visibility: export inject_LT_LTE : LT a b -> LTE a b
- Totality: total
Visibility: export inject_EQ_LTE : EQ a b -> LTE a b
- Totality: total
Visibility: export trans : LTE a b -> LTE b c -> LTE a c
LTE is a transitive relation
Totality: total
Visibility: exportantisym : LTE a b -> LTE b a -> EQ a b
LTE is an antisymmetric relation
Totality: total
Visibility: exportGTE : Int -> Int -> Type
GTE is defined in terms of LTE to avoid code duplication
Totality: total
Visibility: public exporttrichotomous : (a : Int) -> (b : Int) -> Trichotomous LT EQ GT a b
Any pair of Ints is related either via LT, EQ, or GT
Totality: total
Visibility: exportdecide_LT_GTE : (a : Int) -> (b : Int) -> Either (LT a b) (GTE a b)
Any pair of Ints is related either via LT or GTE
Totality: total
Visibility: exportdecide_LTE_GT : (a : Int) -> (b : Int) -> Either (LTE a b) (GT a b)
Any pair of Ints is related either via LTE or GT
Totality: total
Visibility: exportsuc_LT_LTE : LT a b -> LTE (a + 1) b
Adding one to a strictly smaller Int, yields a smaller Int
Totality: total
Visibility: exportpred_LT_LTE : LT a b -> LTE a (b - 1)
Subtracting one to a strictly larger Int, yields a larger Int
Totality: total
Visibility: exportsucBounded : LT a b -> LT a (a + 1)
Adding one to an Int yields a strictly larger one,
provided there is no overflow
Totality: total
Visibility: export