Language.Reflection.Compat.Constr

Reexports

Definitions

normaliseCon : Elaboration m => Con -> m Con

Totality: total
Visibility: export

conSubexprs : Con -> List TTImp

Totality: total
Visibility: export

.sig : Con -> TTImp

  Calculate constructor signature

Totality: total
Visibility: export

.iTy : Con -> ITy

  Calculate constructor ITy

Totality: total
Visibility: export

record ConArg : (0 _ : Con) -> Type

Totality: total
Visibility: public export
Constructor: 

MkConArg : Fin ((con .args) .length) -> ConArg con

Projection: 

.conArgIdx : ConArg con -> Fin ((con .args) .length)

.conArgIdx : ConArg con -> Fin ((con .args) .length)

Totality: total
Visibility: public export

conArgIdx : ConArg con -> Fin ((con .args) .length)

Totality: total
Visibility: public export

fromInteger : (x : Integer) -> {auto 0 _ : So (integerLessThanNat x ((con .args) .length))} -> ConArg con

Totality: total
Visibility: public export

fromName : (n : Name) -> Elem (Just n) (map name (con .args)) => ConArg con

Totality: total
Visibility: public export

.dataCon : Name -> Elab Name

Totality: total
Visibility: export

record IsConstructor : (0 _ : Name) -> Type

Totality: total
Visibility: public export
Constructor: 

ItIsCon : TypeInfo -> Con -> IsConstructor n

Projections:

.conInfo : IsConstructor n -> Con

.typeInfo : IsConstructor n -> TypeInfo

.typeInfo : IsConstructor n -> TypeInfo

Totality: total
Visibility: public export

typeInfo : IsConstructor n -> TypeInfo

Totality: total
Visibility: public export

.conInfo : IsConstructor n -> Con

Totality: total
Visibility: public export

conInfo : IsConstructor n -> Con

Totality: total
Visibility: public export

data GenuineProof : IsConstructor n -> Type

Totality: total
Visibility: export
Constructor: 

ItIsGenuine : GenuineProof iscn

itIsConstructor : Elab (con : IsConstructor n ** GenuineProof con)

Totality: total
Visibility: export