Language.Lean.Inductive

Operations for creating inductive types and declarations.

Inductive type

data InductiveType

An inductive type

Instances

IsLeanValue InductiveType (Ptr InductiveType)

IsList (List InductiveType)

Eq (List InductiveType)

IsListIso (List InductiveType)

IsLeanValue (List InductiveType) (Ptr (List InductiveType))

data List InductiveType = ListInductiveType (ForeignPtr (List InductiveType))

A list of inductive types (constructor not actually exported)

type Item (List InductiveType) = InductiveType

inductiveType

Arguments

:: Name

Name of the inductive type

-> Expr

Type of the inductive type

-> List Expr

Constructors (must be a list of local constants)

-> InductiveType

Creates an inductive type

inductiveTypeName :: InductiveType -> Name

Get the name of a inductive type.

inductiveTypeType :: InductiveType -> Expr

Get the type of a inductive type.

inductiveTypeConstructors :: InductiveType -> List Expr

Get the list of constructors associated with the given inductive type.

recursorName :: Name -> Name

Get the name of the recursor (aka eliminator) associated with a inductive type with given name.

Inductive declarations

data InductiveDecl

An inductive declaration

A single inductive declaration may define one or more Lean inductive types. The inductive types must have the same parameters.

Instances

IsLeanValue InductiveDecl (Ptr InductiveDecl)

inductiveDecl

Arguments

:: List Name

Universe parameters

-> Word32

Number of parameters

-> List InductiveType

List of inductive types

-> InductiveDecl

A inductive datatype declaration

The remaining inductive datatype arguments are treated as indices.

inductiveDeclUnivParams :: InductiveDecl -> List Name

Get the list of universe parameter names for the given inductive declaration.

inductiveDeclNumParams :: InductiveDecl -> Word32

Get the number of parameters for the in the declaration.

inductiveDeclTypes :: InductiveDecl -> List InductiveType

Get the list of inductive types in the inductive declaration

Environment operations

addInductiveDecl :: InductiveDecl -> Env -> Env

Add the inductive declaration to the given environment.

lookupInductiveDecl :: Env -> Name -> Maybe InductiveDecl

Return the inductive declaration that introduced type with the given name in the environment (or Nothing if no inductive type by that name exists).

lookupConstructorInductiveTypeName :: Env -> Name -> Maybe Name

If the given name is a constructor in the envionment, this returns the name of the associated inductive type.

If the name is not a constructor, then this returns Nothing.

lookupRecursorInductiveTypeName :: Env -> Name -> Maybe Name

If the given name is a recursor in the given environment, this returns the name of the associated inductive type.

If the name is not a recursor, then this returns Nothing.

lookupInductiveTypeNumIndices :: Env -> Name -> Maybe Word32

Given the name of an inductive type in the environment, this returns the number of indices.

If the name is not an inductive type, then this returns Nothing.

lookupInductiveTypeNumMinorPremises :: Env -> Name -> Maybe Word32

Given the name of an inductive type in the environment, this returns the number of minor premises for the recursor associated to this type.

If the name is not an inductive type, then this returns Nothing.

inductiveTypeHasDepElim :: Env -> Name -> Bool

Given a name, this returns true if the name is for a inductive type that supports dependent elimination.