Generics.Derive

Reexports

import public Generics.SOP
import public Generics.Meta
import public Decidable.Equality
import public Language.Reflection.Util

  Name of record `Generic`'s constructor.

Totality: total
Visibility: export

mkCode : ParamTypeInfo -> TTImp

  Creates the syntax tree for the code of the given data type.
  We export this since it might be useful elsewhere.

Totality: total
Visibility: export

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

  Derives a `Generic` implementation for the given data type
  and visibility.

Totality: total
Visibility: export

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

  Alias for `GenericVis Public`.

Totality: total
Visibility: export

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

  Derives a `Meta` implementation for the given data type
  and visibility.

Totality: total
Visibility: export

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

  Alias for `EqVis Public`.

Totality: total
Visibility: export

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

  Derives `Eq` for the given data type.
  
  @deprecated : This is deprecated. Use `Derive.Eq.Eq` from elab-util.

Totality: total
Visibility: export

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

  Derives `Ord` for the given data type.
  
  @deprecated : This is deprecated. Use `Derive.Ord.Ord` from elab-util.

Totality: total
Visibility: export

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

  Derives `DecEq` for the given data type.

Totality: total
Visibility: export

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

  Derives `Show` for the given data type.
  
  @deprecated : This is deprecated. Use `Derive.Show.Show` from elab-util.

Totality: total
Visibility: export