Derive.BarbieInfo

Definitions

data ToType : TTImp -> Type

  Proof that a `TTImp` corresponds to `k -> Type` for some `k`.

Totality: total
Visibility: public export
Constructor: 

IsToType : ToType (IPi f1 MW ExplicitArg n2 k (IType f3))

toType : (t : TTImp) -> Maybe (ToType t)

Totality: total
Visibility: public export

data BarbieArgs : Vect n Arg -> Type

  Proof that the last in a list of arguments is of type `Type -> Type`

Totality: total
Visibility: public export
Constructors:

BAHere : ToType t => BarbieArgs [MkArg c ExplicitArg (Just n) t]

BAThere : BarbieArgs vs -> BarbieArgs (v :: vs)

barbieArgs : (vs : Vect n Arg) -> Maybe (BarbieArgs vs)

Totality: total
Visibility: public export

barbieArg : BarbieArgs vs -> Name

  Name of the last argument of a `Barbie` type constructor.

Totality: total
Visibility: public export

barbieKind : BarbieArgs vs -> TTImp

  Name of the last argument of a `Barbie` type constructor.

Totality: total
Visibility: public export

record BarbieInfo : Type

  Proof that a parameterized type is actually a `Barbie`.

Totality: total
Visibility: public export
Constructor: 

BI : (info : ParamTypeInfo) -> BarbieArgs ((info .info) .args) -> BarbieInfo

Projections:

.info : BarbieInfo -> ParamTypeInfo

.prf : ({rec:0} : BarbieInfo) -> BarbieArgs (((info {rec:0}) .info) .args)

Hint: 

Named BarbieInfo

.info : BarbieInfo -> ParamTypeInfo

Totality: total
Visibility: public export

info : BarbieInfo -> ParamTypeInfo

Totality: total
Visibility: public export

.prf : ({rec:0} : BarbieInfo) -> BarbieArgs (((info {rec:0}) .info) .args)

Totality: total
Visibility: public export

prf : ({rec:0} : BarbieInfo) -> BarbieArgs (((info {rec:0}) .info) .args)

Totality: total
Visibility: public export

hasFArg : Name -> TTImp -> Bool

Totality: total
Visibility: public export

.explicitArgs : BarbieInfo -> List Name

  Names of all type arguments of a barbie, except the last one

Totality: total
Visibility: public export

.applied : BarbieInfo -> TTImp

  Returns a type constructor
  applied to the names of its explicit arguments except the last one

Totality: total
Visibility: public export

.implicits : BarbieInfo -> List Arg

  Returns a list of implicit arguments corresponding
  to the data type's explicit arguments (except the last one)

Totality: total
Visibility: public export

.kind : BarbieInfo -> TTImp

  Returns the kind of the first argument of the last parameter of
  a barbie.

Totality: total
Visibility: public export