Processing math: 100%
fin-0.2: Nat and Fin: peano naturals and finite numbers
Safe HaskellSafe
LanguageHaskell2010

Data.Type.Nat.LE.ReflStep

Synopsis

Relation

data LEProof n m where Source #

An evidence of nm. refl+step definition.

Constructors

LERefl :: LEProof n n 
LEStep :: LEProof n m -> LEProof n ('S m) 

Instances

Instances details
Category LEProof Source #

The other variant (LEPRoof) isn't Category, because leRefl requires SNat evidence.

Instance details

Defined in Data.Type.Nat.LE.ReflStep

Methods

id :: forall (a :: k). LEProof a a #

(.) :: forall (b :: k) (c :: k) (a :: k). LEProof b c -> LEProof a b -> LEProof a c #

Eq (LEProof n m) Source #

LEProof values are unique (not Boring though!).

Instance details

Defined in Data.Type.Nat.LE.ReflStep

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.ReflStep

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.ReflStep

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.ReflStep

Methods

decide :: Dec (LEProof n m) #

fromZeroSucc :: forall n m. SNatI m => LEProof n m -> LEProof n m Source #

Convert from zero+succ to refl+step definition.

Inverse of toZeroSucc.

toZeroSucc :: SNatI n => LEProof n m -> LEProof n m Source #

Convert refl+step to zero+succ definition.

Inverse of fromZeroSucc.

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 :: forall n. SNatI n => LEProof 'Z n Source #

n:N,0n

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

nm:N,nm1+n1+m

leRefl :: 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)

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