Idris2Doc : Core.TT.Binder

Core.TT.Binder

(source)
Definitions
data PiInfo : Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Implicit : PiInfo t
  Implicit Pi types (e.g. {0 a : Type} -> ...)
  The argument is to be solved by unification
  
Explicit : PiInfo t
  Explicit Pi types (e.g. (x : a) -> ...)
  The argument is to be passed explicitly
  
AutoImplicit : PiInfo t
  Auto Pi types (e.g. (fun : Functor f) => ...)
  The argument is to be solved by proof search
  
DefImplicit : t -> PiInfo t
  Default Pi types (e.g. {default True flag : Bool} -> ...)
  The argument is set to the default value if nothing is
  passed explicitly

  Hints:
  
Eq t => Eq (PiInfo t)
  
Foldable PiInfo
  
Functor PiInfo
  
Hashable t => Hashable (PiInfo t)
  
Reflect t => Reflect (PiInfo t)
  
Reify t => Reify (PiInfo t)
  
Show t => Show (PiInfo t)
  
TTC t => TTC (PiInfo t)
  
Traversable PiInfo
isImplicit : PiInfo t -> Bool
  Totality: total
  Visibility: export
eqPiInfoBy : (t -> u -> Bool) -> PiInfo t -> PiInfo u -> Bool
  Heterogeneous equality, provided an heterogeneous equality
  of default values

  Totality: total
  Visibility: export
forgetDef : PiInfo t -> PiInfo t'
  Totality: total
  Visibility: export
record PiBindData : Type -> Type
  A bound value along with its `PiInfo`.
  We cannot use `PiInfo` as metadata for `WithData` because the record is functorial in both
  `t` and `PiInfo`.

  Totality: total
  Visibility: public export
  Constructor: 
MkPiBindData : PiInfo t -> t -> PiBindData t

  Projections:
  
.boundType : PiBindData t -> t
  
.info : PiBindData t -> PiInfo t

  Hints:
  
Foldable PiBindData
  
Functor PiBindData
  
Show t => Show (PiBindData t)
  
TTC t => TTC (PiBindData t)
  
Traversable PiBindData
.info : PiBindData t -> PiInfo t
  Totality: total
  Visibility: public export
info : PiBindData t -> PiInfo t
  Totality: total
  Visibility: public export
.boundType : PiBindData t -> t
  Totality: total
  Visibility: public export
boundType : PiBindData t -> t
  Totality: total
  Visibility: public export
mapType : (t -> t) -> PiBindData t -> PiBindData t
  Totality: total
  Visibility: public export
data Binder : Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Lam : FC -> RigCount -> PiInfo type -> type -> Binder type
  
Let : FC -> RigCount -> type -> type -> Binder type
  
Pi : FC -> RigCount -> PiInfo type -> type -> Binder type
  
PVar : FC -> RigCount -> PiInfo type -> type -> Binder type
  
PLet : FC -> RigCount -> type -> type -> Binder type
  
PVTy : FC -> RigCount -> type -> Binder type

  Hints:
  
Eq a => Eq (Binder a)
  
Foldable Binder
  
Functor Binder
  
Hashable ty => Hashable (Binder ty)
  
Show ty => Show (Binder ty)
  
TTC (Binder (Term vars))
  
Traversable Binder
isLet : Binder t -> Bool
  Totality: total
  Visibility: export
binderLoc : Binder tm -> FC
  Totality: total
  Visibility: export
binderType : Binder tm -> tm
  Totality: total
  Visibility: export
multiplicity : Binder tm -> RigCount
  Totality: total
  Visibility: export
piInfo : Binder tm -> PiInfo tm
  Totality: total
  Visibility: export
isImplicit : Binder tm -> Bool
  Totality: total
  Visibility: export
setMultiplicity : Binder tm -> RigCount -> Binder tm
  Totality: total
  Visibility: export
setType : Binder tm -> tm -> Binder tm
  Totality: total
  Visibility: export
eqBinderBy : (t -> u -> Bool) -> Binder t -> Binder u -> Bool
  Totality: total
  Visibility: export