Derive.ApplicativeB

Definitions

bpureClaim : Visibility -> Name -> BarbieInfo -> Decl

Totality: total
Visibility: export

bprodClaim : Visibility -> Name -> BarbieInfo -> Decl

Totality: total
Visibility: export

applicativeImplClaim : Visibility -> Name -> BarbieInfo -> Decl

  Top-level declaration implementing the `Eq` interface for
  the given data type.

Totality: total
Visibility: export

applicativeImplDef : Name -> Name -> Name -> Decl

Totality: total
Visibility: export

prodClause : Name -> Con n vs -> Clause

Totality: total
Visibility: export

prodDef : Name -> Con n vs -> Decl

Totality: total
Visibility: export

pureDef : Name -> Con n vs -> Decl

Totality: total
Visibility: export

ApplicativeBVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)

  Generate declarations and implementations for `ApplicativeB`
  for a given data type.

Totality: total
Visibility: export

ApplicativeB : List Name -> ParamTypeInfo -> Res (List TopLevel)

  Alias for `ApplicativeBVis Public`

Totality: total
Visibility: export