Skip to content

HORIZON HASKELL Docs lts/ghc-10.0.x77a86622026-10-31Search packagesCtrl K

Theme: |

GHC 10.0.0.20260917 · lts/ghc-10.0.x · 77a8662 · 2026-10-31

Modulefin-0.3.2Haskell2010

Data.Type.Nat.LE.ReflStep

Contents

Relation
Decidability
Lemmas
Constructor like
Partial order
Total order
More

Synopsis

data LEProof
value fromZeroSucc
value toZeroSucc
value decideLE
value leZero
value leSucc
value leRefl
value leStep
value leAsym
value leTrans
value leSwap
value leSwap'
value leStepL
value lePred
value proofZeroLEZero

Packagefin-0.3.2
Exports15
LanguageHaskell2010
LicenceBSD-3-Clause
SourceReflStep.hs

Relation

datadata LEProof (n :: Nat) (m :: Nat) where

An evidence of n \le m. refl+step definition.

Constructors

LERefl :: LEProof n n
LEStep :: LEProof n m -> LEProof n m

Instances7Category, Eq, Ord, Show, Absurd, Boring, …

Category LEProofDefined in fin-0.3.2 · Data.Type.Nat.LE.ReflStep
The other variant (Data.Type.Nat.LE.LEPRoof) isn't Category, because leRefl requires SNat evidence.
Eq (LEProof n m)Defined in fin-0.3.2 · Data.Type.Nat.LE.ReflStep
LEProof values are unique (not Boring though!).
Ord (LEProof n m)Defined in fin-0.3.2 · Data.Type.Nat.LE.ReflStep
Show (LEProof n m)Defined in fin-0.3.2 · Data.Type.Nat.LE.ReflStep
(LE m n, n' ~ 'S n, SNatI n) => Absurd (LEProof n' m)Defined in fin-0.3.2 · Data.Type.Nat.LE.ReflStep
(LE n m, SNatI m) => Boring (LEProof n m)Defined in fin-0.3.2 · Data.Type.Nat.LE.ReflStep
(SNatI n, SNatI m) => Decidable (LEProof n m)Defined in fin-0.3.2 · Data.Type.Nat.LE.ReflStep

valuefromZeroSucc :: SNatI m => LEProof n m -> LEProof n m

Convert from zero+succ to refl+step definition.

Inverse of toZeroSucc.

valuetoZeroSucc :: SNatI n => LEProof n m -> LEProof n m

Convert refl+step to zero+succ definition.

Inverse of fromZeroSucc.

Decidability

valuedecideLE :: (SNatI n, SNatI m) => Dec (LEProof n m)

Find the LEProof n m, i.e. compare numbers.

Lemmas

Constructor like

valueleZero :: SNatI n => LEProof 'Z n

\forall n : \mathbb{N}, 0 \le n

valueleSucc :: LEProof n m -> LEProof ('S n) ('S m)

\forall n\, m : \mathbb{N}, n \le m \to 1 + n \le 1 + m

valueleRefl :: LEProof n n

\forall n : \mathbb{N}, n \le n

valueleStep :: LEProof n m -> LEProof n ('S m)

\forall n\, m : \mathbb{N}, n \le m \to n \le 1 + m

Partial order

valueleAsym :: LEProof n m -> LEProof m n -> n :~: m

\forall n\, m : \mathbb{N}, n \le m \to m \le n \to n \equiv m

valueleTrans :: LEProof n m -> LEProof m p -> LEProof n p

\forall n\, m\, p : \mathbb{N}, n \le m \to m \le p \to n \le p

Total order

valueleSwap :: (SNatI n, SNatI m) => Neg (LEProof n m) -> LEProof ('S m) n

\forall n\, m : \mathbb{N}, \neg (n \le m) \to 1 + m \le n

valueleSwap' :: LEProof n m -> LEProof ('S m) n -> void

\forall n\, m : \mathbb{N}, n \le m \to \neg (1 + m \le n)

More

valueleStepL :: LEProof ('S n) m -> LEProof n m

\forall n\, m : \mathbb{N}, 1 + n \le m \to n \le m

valuelePred :: LEProof ('S n) ('S m) -> LEProof n m

\forall n\, m : \mathbb{N}, 1 + n \le 1 + m \to n \le m

valueproofZeroLEZero :: LEProof n 'Z -> n :~: 'Z

\forall n\ : \mathbb{N}, n \le 0 \to n \equiv 0