Core.TT.Term

Definitions

data NameType : Type

Totality: total
Visibility: public export
Constructors:

Bound : NameType

Func : NameType

DataCon : Int -> Nat -> NameType

TyCon : Nat -> NameType

Hints:

Reflect NameType

Reify NameType

Show NameType

TTC NameType

isCon : NameType -> Maybe Nat

Totality: total
Visibility: export

data LazyReason : Type

Totality: total
Visibility: public export
Constructors:

LInf : LazyReason

LLazy : LazyReason

LUnknown : LazyReason

Hints:

Eq LazyReason

Hashable LazyReason

Ord LazyReason

Reflect LazyReason

Reify LazyReason

Scheme LazyReason

Show LazyReason

TTC LazyReason

data UseSide : Type

Totality: total
Visibility: public export
Constructors:

UseLeft : UseSide

UseRight : UseSide

Hint: 

TTC UseSide

data WhyErased : Type -> Type

Totality: total
Visibility: public export
Constructors:

Placeholder : WhyErased a

Impossible : WhyErased a

Dotted : a -> WhyErased a

Hints:

Eq a => Eq (WhyErased a)

Foldable WhyErased

Functor WhyErased

Show a => Show (WhyErased a)

Traversable WhyErased

data Term : Scoped

Totality: total
Visibility: public export
Constructors:

Local : FC -> Maybe Bool -> (idx : Nat) -> (0 _ : IsVar name idx vars) -> Term vars

Ref : FC -> NameType -> Name -> Term vars

Meta : FC -> Name -> Int -> List (Term vars) -> Term vars

Bind : FC -> (x : Name) -> Binder (Term vars) -> Term (bind vars x) -> Term vars

App : FC -> Term vars -> Term vars -> Term vars

As : FC -> UseSide -> Term vars -> Term vars -> Term vars

TDelayed : FC -> LazyReason -> Term vars -> Term vars

TDelay : FC -> LazyReason -> Term vars -> Term vars -> Term vars

TForce : FC -> LazyReason -> Term vars -> Term vars

PrimVal : FC -> Constant -> Term vars

Erased : FC -> WhyErased (Term vars) -> Term vars

TType : FC -> Name -> Term vars

Hints:

Convert Term

Eq (Term vars)

FreelyEmbeddable Term

GenWeaken Term

HasNames (Term vars)

HasNames (Env Term vars)

Hashable (Term vars)

IsScoped Term

Quote Term

Show (Term vars)

StripNamespace (Term vars)

TTC (Binder (Term vars))

TTC (Term vars)

TTC (Env Term vars)

Unify Term

Weaken Term

ClosedTerm : Type

Totality: total
Visibility: public export

insertNames : GenWeakenable Term

Visibility: export

compatTerm : CompatibleVars xs ys -> Term xs -> Term ys

Totality: total
Visibility: export

shrinkPi : Shrinkable (PiInfo . Term)

Totality: total
Visibility: export

shrinkBinder : Shrinkable (Binder . Term)

Totality: total
Visibility: export

shrinkTerms : Shrinkable (List . Term)

Totality: total
Visibility: export

thinPi : Thinnable (PiInfo . Term)

Totality: total
Visibility: export

thinBinder : Thinnable (Binder . Term)

Totality: total
Visibility: export

thinTerms : Thinnable (List . Term)

Totality: total
Visibility: export

WeakenTerm : Weaken Term

Totality: total
Visibility: export

apply : FC -> Term vars -> List (Term vars) -> Term vars

Totality: total
Visibility: export

applySpineWithFC : Term vars -> SnocList (FC, Term vars) -> Term vars

Totality: total
Visibility: export

applyStackWithFC : Term vars -> List (FC, Term vars) -> Term vars

Totality: total
Visibility: export

fnType : FC -> Term vars -> Term vars -> Term vars

Totality: total
Visibility: export

linFnType : FC -> Term vars -> Term vars -> Term vars

Totality: total
Visibility: export

getFnArgs : Term vars -> (Term vars, List (Term vars))

Totality: total
Visibility: export

getFn : Term vars -> Term vars

Totality: total
Visibility: export

getArgs : Term vars -> List (Term vars)

Totality: total
Visibility: export

interface StripNamespace : Type -> Type

Parameters: a
Methods:

trimNS : Namespace -> a -> a

restoreNS : Namespace -> a -> a

Implementations:

StripNamespace (CaseTree vars)

StripNamespace (CaseAlt vars)

StripNamespace Name

StripNamespace (Term vars)

StripNamespace Def

StripNamespace GlobalDef

trimNS : StripNamespace a => Namespace -> a -> a

Totality: total
Visibility: public export

restoreNS : StripNamespace a => Namespace -> a -> a

Totality: total
Visibility: public export

isErased : Term vars -> Bool

Totality: total
Visibility: export

getLoc : Term vars -> FC

Totality: total
Visibility: export

compatible : LazyReason -> LazyReason -> Bool

Totality: total
Visibility: export

eqWhyErasedBy : (a -> b -> Bool) -> WhyErased a -> WhyErased b -> Bool

Totality: total
Visibility: export

eqTerm : Term vs -> Term vs' -> Bool

Totality: total
Visibility: export

resolveNames : (vars : Scope) -> Term vars -> Term vars

Totality: total
Visibility: export

withPiInfo : Show t => PiInfo t -> String -> String

Totality: total
Visibility: export