Skip to content

HORIZON HASKELL Docs lts/ghc-10.0.xfc4e5982026-10-11Search names, modules, packages, or :: a typeCtrl K

GHC 10.0.0.20260917 · lts/ghc-10.0.x · fc4e598 · 2026-10-11

Modulefin-0.3.2Haskell2010

Data.Type.Nat.LE.ReflStep

1 type
14 values

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

Relation

3 declarations

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

1 declaration

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

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

Lemmas

0 declarations

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