levmar-0.2.1: An implementation of the Levenberg-Marquardt algorithmSource codeContentsIndex
TypeLevelNat
Synopsis
data Z = Z
newtype S n = S n
class Nat n where
caseNat :: forall r. n -> (n ~ Z => r) -> (forall p. (n ~ S p, Nat p) => p -> r) -> r
induction :: forall p n. Nat n => n -> p Z -> (forall m. Nat m => p m -> p (S m)) -> p n
witnessNat :: forall n. Nat n => n
data N n where
Zero :: N Z
Succ :: N n -> N (S n)
nat :: forall n. Nat n => n -> N n
Documentation
data Z Source
Type-level natural denoting zero
Constructors
Z
show/hide Instances
newtype S n Source
Type-level natural denoting the Successor of another type-level natural.
Constructors
S n
show/hide Instances
Show n => Show (S n)
Nat p => Nat (S p)
ComposeN n => ComposeN (S n)
class Nat n whereSource
Class of all type-level naturals.
Methods
caseNatSource
:: forall r .
=> nThe natural number to case analyse.
-> n ~ Z => rThe result r when n equals zero.
-> forall p. (n ~ S p, Nat p) => p -> rFunction to apply to the predecessor of n to yield the result r.
-> r
Case analysis on natural numbers.
show/hide Instances
Nat Z
Nat p => Nat (S p)
induction :: forall p n. Nat n => n -> p Z -> (forall m. Nat m => p m -> p (S m)) -> p nSource
The axiom of induction on natural numbers. See: http://en.wikipedia.org/wiki/Mathematical_induction#Axiom_of_induction
witnessNat :: forall n. Nat n => nSource

The value of witnessNat :: n is the natural number of type n. For example: 

 *TypeLevelNat> witnessNat :: S (S (S Z))
 S (S (S Z))
data N n whereSource
A value-level natural indexed with an equivalent type-level natural.
Constructors
Zero :: N Z
Succ :: N n -> N (S n)
nat :: forall n. Nat n => n -> N nSource
Produced by Haddock version 2.4.2