Language.Reflection

userSuppliedName : String -> TTName

reflectConstant : ReflConst a => a -> Const

quoteRawBinder : Binder Raw -> TT

quoteRaw : Raw -> TT

data Universe : Type

Universes

NullType : Universe

UniqueType : Universe

AllTypes : Universe

data Tactic : Type

A representation of Idris's tactics that can be returned from custom
tactic implementations. Generate these using applyTactic.

Try : Tactic -> Tactic -> Tactic

Try the first tactic and resort to the second one on failure

GoalType : String -> Tactic -> Tactic

Only run if the goal has the right type

Refine : TTName -> Tactic

Resolve function name, find matching arguments in the
context and compute the proof target

Seq : Tactic -> Tactic -> Tactic

Apply both tactics in sequence

Claim : TTName -> TT -> Tactic

Introduce a new hole with a particular type

Unfocus : Tactic

Move the current hole to the end

Trivial : Tactic

Intelligently construct the proof target from the context

Search : Int -> Tactic

Build a proof by applying contructors up to a maximum depth

Instance : Tactic

Resolve a type class

Solve : Tactic

Infer the proof target from the context

Intros : Tactic

introduce all variables into the context

Intro : TTName -> Tactic

Introduce a named variable into the context, use the
first one if the given name is not found

ApplyTactic : TT -> Tactic

Invoke the reflected rep. of another tactic

Reflect : TT -> Tactic

Turn a value into its reflected representation

ByReflection : TT -> Tactic

Use a %reflection function

Fill : Raw -> Tactic

Turn a raw value back into a term

Exact : TT -> Tactic

Use the given value to conclude the proof

Focus : TTName -> Tactic

Focus on a particular hole

Rewrite : TT -> Tactic

Rewrite with an equality

Induction : TT -> Tactic

Perform induction on a particular expression

Case : TT -> Tactic

Perform case analysis on a particular expression

LetTac : TTName -> TT -> Tactic

Name a reflected term

LetTacTy : TTName -> TT -> TT -> Tactic

Name a reflected term and type it

Compute : Tactic

Normalise the goal

Skip : Tactic

Do nothing

Fail : List ErrorReportPart -> Tactic

Fail with an error message

SourceFC : Tactic

Attempt to fill the hole with source code information

data TTUExp : Type

UVar : Int -> TTUExp

Universe variable

UVal : Int -> TTUExp

Explicit universe level

data TTName : Type

UN : String -> TTName

A user-provided name

NS : TTName -> List String -> TTName

A name in some namespace.

The namespace is in reverse order, so (NS (UN "foo") ["B", "A"])
represents the name A.B.foo

MN : Int -> String -> TTName

Machine-chosen names

SN : SpecialName -> TTName

Special names, to make conflicts impossible and language features
predictable

NErased : TTName

Name of something which is never used in scope

data TT : Type

Reflection of the well typed core language

P : NameType -> TTName -> TT -> TT

A reference to some name (P for Parameter)

V : Int -> TT

de Bruijn variables

Bind : TTName -> Binder TT -> TT -> TT

Bind a variable

App : TT -> TT -> TT

Apply one term to another

TConst : Const -> TT

Embed a constant

Proj : TT -> Int -> TT

Argument projection; runtime only

Erased : TT

Erased terms

Impossible : TT

Impossible terms

TType : TTUExp -> TT

The type of types along (with universe constraints)

UType : Universe -> TT

data SpecialName : Type

WhereN : Int -> TTName -> TTName -> SpecialName

WithN : Int -> TTName -> SpecialName

InstanceN : TTName -> List String -> SpecialName

ParentN : TTName -> String -> SpecialName

MethodN : TTName -> SpecialName

CaseN : TTName -> SpecialName

ElimN : TTName -> SpecialName

InstanceCtorN : TTName -> SpecialName

MetaN : TTName -> TTName -> SpecialName

data SourceLocation : Type

FileLoc : (filename : String) -> (start : (Int, Int)) -> (end : (Int, Int)) -> SourceLocation

class ReflConst 

toConst : ReflConst a => a -> Const

data Raw : Type

Raw terms without types

Var : TTName -> Raw

Variables, global or local

RBind : TTName -> Binder Raw -> Raw -> Raw

Bind a variable

RApp : Raw -> Raw -> Raw

Application

RType : Raw

The type of types

RUType : Universe -> Raw

RForce : Raw -> Raw

RConstant : Const -> Raw

Embed a constant

class Quotable 

Things with a canonical representation as a reflected term.

This type class is intended to be used during proof automation and the
construction of custom tactics.

quotedTy : Quotable a t => t

A representation of the type a.

This is to enable quoting polymorphic datatypes

quote : Quotable a t => a -> t

Quote a particular element of a.

Each equation should look something like quote (Foo x y) = `(Foo ~(quote x) ~(quote y))

data NativeTy : Type

IT8 : NativeTy

IT16 : NativeTy

IT32 : NativeTy

IT64 : NativeTy

data NameType : Type

Types of named references

Bound : NameType

A reference which is just bound, e.g. by intro

Ref : NameType

A reference to a de Bruijn-indexed variable

DCon : Int -> Int -> NameType

Data constructor with tag and number

TCon : Int -> Int -> NameType

Type constructor with tag and number

data IntTy : Type

ITFixed : NativeTy -> IntTy

ITNative : IntTy

ITBig : IntTy

ITChar : IntTy

data ErrorReportPart : Type

Error reports are a list of report parts

TextPart : String -> ErrorReportPart

A human-readable string

NamePart : TTName -> ErrorReportPart

An Idris name (to be semantically coloured)

TermPart : TT -> ErrorReportPart

An Idris term, to be pretty printed

SubReport : List ErrorReportPart -> ErrorReportPart

An indented sub-report, to provide more details

data Const : Type

Primitive constants

I : Int -> Const

BI : Integer -> Const

Fl : Double -> Const

Ch : Char -> Const

Str : String -> Const

B8 : Bits8 -> Const

B16 : Bits16 -> Const

B32 : Bits32 -> Const

B64 : Bits64 -> Const

AType : ArithTy -> Const

StrType : Const

VoidType : Const

Forgot : Const

WorldType : Const

TheWorld : Const

data Binder : Type -> Type

Types annotations for bound variables in different
binding contexts

Lam : a -> Binder a

Pi : a -> a -> Binder a

Let : a -> a -> Binder a

NLet : a -> a -> Binder a

Hole : a -> Binder a

GHole : a -> Binder a

Guess : a -> a -> Binder a

PVar : a -> Binder a

PVTy : a -> Binder a

data ArithTy : Type

ATInt : IntTy -> ArithTy

ATFloat : ArithTy