Core.Reflect

Definitions

interface Reify : Type -> Type

Parameters: a
Methods:

reify : Ref Ctxt Defs => Defs -> NF vars -> Core a

Implementations:

Reify ()

Reify String

Reify Int

Reify Int8

Reify Int16

Reify Int32

Reify Int64

Reify Bits8

Reify Bits16

Reify Bits32

Reify Bits64

Reify Integer

Reify Char

Reify Double

Reify Bool

Reify Nat

Reify a => Reify (List a)

Reify a => Reify (List1 a)

Reify a => Reify (SnocList a)

Reify a => Reify (Maybe a)

Reify a => Reify (WithDefault a def)

(Reify a, Reify b) => Reify (a, b)

Reify Namespace

Reify ModuleIdent

Reify UserName

Reify Name

Reify NameType

Reify PrimType

Reify Constant

Reify Visibility

Reify TotalReq

Reify RigCount

Reify t => Reify (PiInfo t)

Reify LazyReason

Reify VirtualIdent

Reify BuiltinType

Reify OriginDesc

Reify FC

Reify a => Reify (WithFC a)

reify : Reify a => Ref Ctxt Defs => Defs -> NF vars -> Core a

Visibility: public export

interface Reflect : Type -> Type

Parameters: a
Methods:

reflect : FC -> Defs -> Bool -> Env Term vars -> a -> Core (Term vars)

Implementations:

Reflect ()

Reflect String

Reflect Int

Reflect Int8

Reflect Int16

Reflect Int32

Reflect Int64

Reflect Bits8

Reflect Bits16

Reflect Bits32

Reflect Bits64

Reflect Integer

Reflect Char

Reflect Double

Reflect Bool

Reflect Nat

Reflect a => Reflect (List a)

Reflect a => Reflect (List1 a)

Reflect a => Reflect (SnocList a)

Reflect a => Reflect (Maybe a)

Reflect a => Reflect (WithDefault a def)

(Reflect a, Reflect b) => Reflect (a, b)

Reflect Namespace

Reflect ModuleIdent

Reflect UserName

Reflect Name

Reflect NameType

Reflect PrimType

Reflect Constant

Reflect Visibility

Reflect TotalReq

Reflect RigCount

Reflect t => Reflect (PiInfo t)

Reflect LazyReason

Reflect BuiltinType

Reflect VirtualIdent

Reflect OriginDesc

Reflect FC

Reflect a => Reflect (WithFC a)

reflect : Reflect a => FC -> Defs -> Bool -> Env Term vars -> a -> Core (Term vars)

Visibility: public export

getCon : FC -> Defs -> Name -> Core (Term vars)

Visibility: export

appCon : FC -> Defs -> Name -> List (Term vars) -> Core (Term vars)

Visibility: export

preludetypes : String -> Name

Visibility: export

basics : String -> Name

Visibility: export

builtin : String -> Name

Visibility: export

primio : String -> Name

Visibility: export

reflection : String -> Name

Visibility: export

reflectiontt : String -> Name

Visibility: export

reflectionttimp : String -> Name

Visibility: export

cantReify : Ref Ctxt Defs => NF vars -> String -> Core a

Visibility: export

cantReflect : FC -> String -> Core a

Visibility: export