Res : Type -> Type- Totality: total
Visibility: public export record Con : Type Constructor of a data type
Totality: total
Visibility: public export
Constructor: MkCon : Name -> List NamedArg -> TTImp -> Con
Projections:
.args : Con -> List NamedArg.name : Con -> Name.type : Con -> TTImp
Hint: Pretty Con
.name : Con -> Name- Totality: total
Visibility: public export name : Con -> Name- Totality: total
Visibility: public export .args : Con -> List NamedArg- Totality: total
Visibility: public export args : Con -> List NamedArg- Totality: total
Visibility: public export .type : Con -> TTImp- Totality: total
Visibility: public export type : Con -> TTImp- Totality: total
Visibility: public export getCon : Elaboration m => Name -> m Con Tries to lookup a constructor by name.
Totality: total
Visibility: exportrecord TypeInfo : Type Information about a data type
@name : Name of the data type
Note: There is no guarantee that the name will be fully
qualified
@args : Type arguments of the data type
@cons : List of data constructors
Totality: total
Visibility: public export
Constructor: MkTypeInfo : Name -> List NamedArg -> List Con -> TypeInfo
Projections:
.args : TypeInfo -> List NamedArg.cons : TypeInfo -> List Con.name : TypeInfo -> Name
Hint: Pretty TypeInfo
.name : TypeInfo -> Name- Totality: total
Visibility: public export name : TypeInfo -> Name- Totality: total
Visibility: public export .args : TypeInfo -> List NamedArg- Totality: total
Visibility: public export args : TypeInfo -> List NamedArg- Totality: total
Visibility: public export .cons : TypeInfo -> List Con- Totality: total
Visibility: public export cons : TypeInfo -> List Con- Totality: total
Visibility: public export getInfo' : Elaboration m => Name -> m TypeInfo Tries to get information about the data type specified
by name. The name need not be fully qualified, but
needs to be unambiguous.
Totality: total
Visibility: exportgetInfo : Name -> Elab TypeInfo macro version of `getInfo'`
Totality: total
Visibility: exportsingleCon : Name -> Elab Name Tries to get the name of the sole constructor
of data type specified by name. Fails, if
the name is not unambiguous, or if the data type
in question has not exactly one constructor.
Totality: total
Visibility: exportrecord ExplicitArg : Type Explicit arg of a data constructor
The `hasParam` flag indicates, whether one of the
type parameters of the data type makes an appearance
in the arguments type.
For instance, in the following data type, arguments
a1 and a3 would have `hasParam` set to `True`.
```
data MyData : (f : Type -> Type) -> (t : Type) -> Type where
A : (a1 : f Int) -> (a2 : String) -> MyData f a
B : (a3 : f a) -> MyData f a
```
Totality: total
Visibility: public export
Constructor: MkExplicitArg : Name -> TTImp -> List TTImp -> Bool -> ExplicitArg
Projections:
.isRecursive : ExplicitArg -> Bool True if the name of the data type itself
makes an appearance in `tpe`
.name : ExplicitArg -> Name Name of the argument
.paramTypes : ExplicitArg -> List TTImp List of types occuring in `tpe` whose outermost
type constructor is a parameter.
Two examples:
If `tpe` is `Foo a (Maybe b)`, this is `[a,b]`
if `tpe` is `Bar (f Int) c`, this is `[f Int,c]`
.tpe : ExplicitArg -> TTImp Argument's type as a `TTImp` tree
Hint: Pretty ExplicitArg
.name : ExplicitArg -> Name Name of the argument
Totality: total
Visibility: public exportname : ExplicitArg -> Name Name of the argument
Totality: total
Visibility: public export.tpe : ExplicitArg -> TTImp Argument's type as a `TTImp` tree
Totality: total
Visibility: public exporttpe : ExplicitArg -> TTImp Argument's type as a `TTImp` tree
Totality: total
Visibility: public export.paramTypes : ExplicitArg -> List TTImp List of types occuring in `tpe` whose outermost
type constructor is a parameter.
Two examples:
If `tpe` is `Foo a (Maybe b)`, this is `[a,b]`
if `tpe` is `Bar (f Int) c`, this is `[f Int,c]`
Totality: total
Visibility: public exportparamTypes : ExplicitArg -> List TTImp List of types occuring in `tpe` whose outermost
type constructor is a parameter.
Two examples:
If `tpe` is `Foo a (Maybe b)`, this is `[a,b]`
if `tpe` is `Bar (f Int) c`, this is `[f Int,c]`
Totality: total
Visibility: public export.isRecursive : ExplicitArg -> Bool True if the name of the data type itself
makes an appearance in `tpe`
Totality: total
Visibility: public exportisRecursive : ExplicitArg -> Bool True if the name of the data type itself
makes an appearance in `tpe`
Totality: total
Visibility: public exportrecord ParamCon : Type Constructor of a parameterized data type.
We only accept two types of arguments for
such a constructor: Implicit arguments
corresponding to the parameters of the data types
and explicit arguments.
See `ParamTypeInfo` for examples about what is
allowed and what not.
Totality: total
Visibility: public export
Constructor: MkParamCon : Name -> List ExplicitArg -> ParamCon
Projections:
.explicitArgs : ParamCon -> List ExplicitArg.name : ParamCon -> Name
Hint: Pretty ParamCon
.name : ParamCon -> Name- Totality: total
Visibility: public export name : ParamCon -> Name- Totality: total
Visibility: public export .explicitArgs : ParamCon -> List ExplicitArg- Totality: total
Visibility: public export explicitArgs : ParamCon -> List ExplicitArg- Totality: total
Visibility: public export record ParamTypeInfo : Type Information about a parameterized data type.
The constructors of such a data type are only
allowed to have two kinds of arguments:
Implicit arguments corresponding to the data
type's parameters and explicit arguments.
Auto implicits or existentials are not allowed.
Below are some examples of valid parameterized data types
```
data Foo a = Val a | Nope
data Reader : (m : Type -> Type) -> (e : Type) -> (a : Type) -> Type where
MkReader : (run : e -> m a) -> Reader m e a
data Wrapper : (n : Nat) -> (t : Type) -> Type
Wrap : Vect n t -> Wrapper n t
```
Examples of invalid parameterized data types
Indexed types families:
```
data GADT : (t : Type) -> Type where
A : GADT Int
B : GADT ()
Any : a -> GADT a
```
Existentials:
```
data Forget : Type where
DoForget : a -> Forget
```
Constraint types:
```
data ShowableForget : Type where
ShowForget : Show a => a -> Forget
```
Totality: total
Visibility: public export
Constructor: MkParamTypeInfo : Name -> List (Name, TTImp) -> List ParamCon -> ParamTypeInfo
Projections:
.cons : ParamTypeInfo -> List ParamCon.name : ParamTypeInfo -> Name.params : ParamTypeInfo -> List (Name, TTImp)
Hint: Pretty ParamTypeInfo
.name : ParamTypeInfo -> Name- Totality: total
Visibility: public export name : ParamTypeInfo -> Name- Totality: total
Visibility: public export .params : ParamTypeInfo -> List (Name, TTImp)- Totality: total
Visibility: public export params : ParamTypeInfo -> List (Name, TTImp)- Totality: total
Visibility: public export .cons : ParamTypeInfo -> List ParamCon- Totality: total
Visibility: public export cons : ParamTypeInfo -> List ParamCon- Totality: total
Visibility: public export calcArgTypesWithParams : ParamTypeInfo -> List TTImp Given the constructor arguments of a data type, returns
the list of those argument types, in which at least one
of the data type's parameters makes an appearance.
This function uses a rudimentary comparison to make
sure that the returned list contains only distinct types.
This function is used to calculate the list of required constraints
when automatically deriving interface implementations.
Totality: total
Visibility: exportgetParamInfo' : Elaboration m => Name -> m ParamTypeInfo Returns information about a parameterized data type
specified by the given (probably not fully qualified) name.
The implementation makes sure, that all occurences of
type parameters in the constructors have been given
the same names as occurences in the type declaration.
Totality: total
Visibility: exportgetParamInfo : Name -> Elab ParamTypeInfo macro version of `getParamInfo`.
Totality: total
Visibility: export