Core.WithData

Reexports

Definitions

Bind' : KeyVal

  The "bind" label containing binding information for metadata records

Visibility: public export

.bind : {auto 0 _ : NameInRange "bind" fields = Just (n, BindingModifier)} -> WithData fields a -> BindingModifier

  Obtain binding information from the metadata

Visibility: export

Arity' : KeyVal

  function arity

Visibility: public export

WithArity : Type -> Type

Visibility: public export

.arity : {auto 0 _ : NameInRange "arity" fields = Just (n, Nat)} -> WithData fields a -> Nat

  Obtain arity information from the metadata

Visibility: export

Opts' : KeyVal

  data constructor options

Visibility: public export

WithOpts : Type -> Type

Visibility: public export

.opts : {auto 0 _ : NameInRange "opts" fields = Just (n, List DataOpt)} -> WithData fields a -> List DataOpt

  Obtain data options from the metadata

Visibility: export

Tot' : KeyVal

  The "totalReq" label containing totality information for metadata records

Visibility: public export

.totReq : {auto 0 _ : NameInRange "totalReq" fields = Just (n, Maybe TotalReq)} -> WithData fields a -> Maybe TotalReq

  Obtain totality information from the metadata

Visibility: export

FC' : KeyVal

  The "fc" label containing file context information for metadata records

Visibility: public export

WithFC : Type -> Type

  Attach FC information to a type

Visibility: public export

AddFC : Type -> Type

Visibility: public export

.fc : NameInRange "fc" fields = Just (n, FC) => WithData fields a -> FC

  Obtain file context information from the metadata

Visibility: export

setFC : NameInRange "fc" fields = Just (n, FC) => FC -> WithData fields a -> WithData fields a

Visibility: export

MkFCVal : FC -> ty -> WithFC ty

  A wrapper for a value with a file context.

Visibility: public export

NoFC : a -> WithFC a

  Smart constructor for WithFC that uses EmptyFC as location

Visibility: export

.withFC : OriginDesc => WithBounds t -> WithFC t

Visibility: export

.addFC : OriginDesc => WithBounds (WithData ls t) -> WithData (FC' :: ls) t

Visibility: export

Doc' : KeyVal

  The "doc" label containing documentation information for metadata records

Visibility: public export

WithDoc : Type -> Type

Visibility: public export

.doc : NameInRange "doc" fields = Just (n, String) => WithData fields a -> String

  Obtain documentation information from the metadata

Visibility: export

Rig' : KeyVal

  The "rig" label containing quantity information for metadata records

Visibility: public export

WithRig : Type -> Type

Visibility: public export

.rig : NameInRange "rig" fields = Just (n, RigCount) => WithData fields a -> RigCount

  Obtain quantity information from the metadata

Visibility: export

Name' : KeyVal

  The "name" label containing a `Name` for metadata records

Visibility: public export

.name : NameInRange "name" fields = Just (n, WithFC Name) => WithData fields a -> WithFC Name

  Extract the name out of the metadata.

Visibility: export

.nameVal : NameInRange "name" fields = Just (n, WithFC Name) => WithData fields a -> Name

  Extract the name out of the metadata.

Visibility: export

WithName : Type -> Type

  Attach name and file context information to a type

Visibility: public export

TyName' : KeyVal

  the "tyname" label containing a `WithFC Name` for metadata records. Typically used for type names.

Visibility: public export

.tyName : NameInRange "tyname" fields = Just (n, WithFC Name) => WithData fields a -> WithFC Name

  Extract the "tyname" value from the metadata record

Visibility: export

DocBindFC : Type -> Type

  Attach documentation, binding and location information to a type

Visibility: public export

MName' : KeyVal

  the "mname" label containing a `Maybe (WithFC Name)` for metadata records

Visibility: public export

WithMName : Type -> Type

Visibility: public export

.mName : NameInRange "mname" fields = Just (n, Maybe (WithFC Name)) => WithData fields a -> Maybe (WithFC Name)

Visibility: export

Names' : KeyVal

  the "names" label containing a `List (WithFC Name)` for metadata records

Visibility: public export

WithNames : Type -> Type

Visibility: public export

.names : NameInRange "names" fields = Just (n, List (WithFC Name)) => WithData fields a -> List (WithFC Name)

Visibility: export