Loading [MathJax]/jax/output/HTML-CSS/jax.js

fin-0.0.3: Nat and Fin: peano naturals and finite numbers

Safe HaskellNone
LanguageHaskell2010

Data.Type.Nat.LE

Contents

Description

Less-than-or-equal relation for (unary) natural numbers Nat.

There are at least three ways to encode this relation.

  • zero:0m and succ:nm1+n1+m (this module),
  • refl:nn and step:nmn1+m (Data.Type.Nat.LE.ReflStep),
  • ex:p.n+pm (tricky in Haskell).

Depending on a situation, usage ergonomics are different.

Synopsis

Relation

class LE n m where Source #

Total order of Nat, less-than-or-Equal-to, .

Methods

leProof :: LEProof n m Source #

Instances
LE Z m Source # 
Instance details

Defined in Data.Type.Nat.LE

Methods

leProof :: LEProof Z m Source #

(m ~ S m', LE n m') => LE (S n) m Source # 
Instance details

Defined in Data.Type.Nat.LE

Methods

leProof :: LEProof (S n) m Source #

data LEProof n m where Source #

An evidence of nm. zero+succ definition.

Constructors

LEZero :: LEProof Z m 
LESucc :: LEProof n m -> LEProof (S n) (S m) 
Instances
Eq (LEProof n m) Source #

LEProof values are unique (not Boring though!).

Instance details

Defined in Data.Type.Nat.LE

Methods

(==) :: LEProof n m -> LEProof n m -> Bool #

(/=) :: LEProof n m -> LEProof n m -> Bool #

Ord (LEProof n m) Source # 
Instance details

Defined in Data.Type.Nat.LE

Methods

compare :: LEProof n m -> LEProof n m -> Ordering #

(<) :: LEProof n m -> LEProof n m -> Bool #

(<=) :: LEProof n m -> LEProof n m -> Bool #

(>) :: LEProof n m -> LEProof n m -> Bool #

(>=) :: LEProof n m -> LEProof n m -> Bool #

max :: LEProof n m -> LEProof n m -> LEProof n m #

min :: LEProof n m -> LEProof n m -> LEProof n m #

Show (LEProof n m) Source # 
Instance details

Defined in Data.Type.Nat.LE

Methods

showsPrec :: Int -> LEProof n m -> ShowS #

show :: LEProof n m -> String #

showList :: [LEProof n m] -> ShowS #

(SNatI n, SNatI m) => Decidable (LEProof n m) Source # 
Instance details

Defined in Data.Type.Nat.LE

Methods

decide :: Dec (LEProof n m) #

withLEProof :: LEProof n m -> (LE n m => r) -> r Source #

Constructor LE dictionary from LEProof.

Decidability

decideLE :: forall n m. (SNatI n, SNatI m) => Dec (LEProof n m) Source #

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

Lemmas

Constructor like

leZero :: LEProof Z n Source #

n:N,0n

leSucc :: LEProof n m -> LEProof (S n) (S m) Source #

nm:N,nm1+n1+m

leRefl :: forall n. SNatI n => LEProof n n Source #

n:N,nn

leStep :: LEProof n m -> LEProof n (S m) Source #

nm:N,nmn1+m

Partial order

leAsym :: LEProof n m -> LEProof m n -> n :~: m Source #

nm:N,nmmnnm

leTrans :: LEProof n m -> LEProof m p -> LEProof n p Source #

nmp:N,nmmpnp

Total order

leSwap :: forall n m. (SNatI n, SNatI m) => Neg (LEProof n m) -> LEProof (S m) n Source #

nm:N,¬(nm)1+mn

leSwap' :: LEProof n m -> LEProof (S m) n -> void Source #

nm:N,nm¬(1+mn)

>>> leProof :: LEProof Nat2 Nat3
LESucc (LESucc LEZero)
>>> leSwap (leSwap' (leProof :: LEProof Nat2 Nat3))
LESucc (LESucc (LESucc LEZero))
>>> lePred (leSwap (leSwap' (leProof :: LEProof Nat2 Nat3)))
LESucc (LESucc LEZero)

More

leStepL :: LEProof (S n) m -> LEProof n m Source #

nm:N,1+nmnm

lePred :: LEProof (S n) (S m) -> LEProof n m Source #

nm:N,1+n1+mnm

proofZeroLEZero :: LEProof n Z -> n :~: Z Source #

n :N,n0n0