TTImp.TTImp

Reexports

Definitions

record NestedNames : Scope -> Type

Totality: total
Visibility: public export
Constructor: 

MkNested : List (Name, (Maybe Name, (List (Var vars), FC -> NameType -> Term vars))) -> NestedNames vars

Projection: 

.names : NestedNames vars -> List (Name, (Maybe Name, (List (Var vars), FC -> NameType -> Term vars)))

Hint: 

Weaken NestedNames

.names : NestedNames vars -> List (Name, (Maybe Name, (List (Var vars), FC -> NameType -> Term vars)))

Visibility: public export

names : NestedNames vars -> List (Name, (Maybe Name, (List (Var vars), FC -> NameType -> Term vars)))

Visibility: public export

mapNestedName : NestedNames vars -> Name -> Name

Visibility: export

data BindMode : Type

Totality: total
Visibility: public export
Constructors:

PI : RigCount -> BindMode

PATTERN : BindMode

COVERAGE : BindMode

NONE : BindMode

Hints:

Reflect BindMode

Reify BindMode

TTC BindMode

RawImp : Type

Visibility: public export

IRawImp : Type

Visibility: public export

data RawImp' : Type -> Type

Totality: total
Visibility: public export
Constructors:

IVar : FC -> nm -> RawImp' nm

IPi : FC -> RigCount -> PiInfo (RawImp' nm) -> Maybe Name -> RawImp' nm -> RawImp' nm -> RawImp' nm

ILam : FC -> RigCount -> PiInfo (RawImp' nm) -> Maybe Name -> RawImp' nm -> RawImp' nm -> RawImp' nm

ILet : FC -> FC -> RigCount -> Name -> RawImp' nm -> RawImp' nm -> RawImp' nm -> RawImp' nm

ICase : FC -> List (FnOpt' nm) -> RawImp' nm -> RawImp' nm -> List (ImpClause' nm) -> RawImp' nm

ILocal : FC -> List (ImpDecl' nm) -> RawImp' nm -> RawImp' nm

ICaseLocal : FC -> Name -> Name -> List Name -> RawImp' nm -> RawImp' nm

IUpdate : FC -> List (IFieldUpdate' nm) -> RawImp' nm -> RawImp' nm

IApp : FC -> RawImp' nm -> RawImp' nm -> RawImp' nm

IAutoApp : FC -> RawImp' nm -> RawImp' nm -> RawImp' nm

INamedApp : FC -> RawImp' nm -> Name -> RawImp' nm -> RawImp' nm

IWithApp : FC -> RawImp' nm -> RawImp' nm -> RawImp' nm

ISearch : FC -> Nat -> RawImp' nm

IAlternative : FC -> AltType' nm -> List (RawImp' nm) -> RawImp' nm

IRewrite : FC -> RawImp' nm -> RawImp' nm -> RawImp' nm

ICoerced : FC -> RawImp' nm -> RawImp' nm

IBindHere : FC -> BindMode -> RawImp' nm -> RawImp' nm

IBindVar : FC -> Name -> RawImp' nm

IAs : FC -> FC -> UseSide -> Name -> RawImp' nm -> RawImp' nm

IMustUnify : FC -> DotReason -> RawImp' nm -> RawImp' nm

IDelayed : FC -> LazyReason -> RawImp' nm -> RawImp' nm

IDelay : FC -> RawImp' nm -> RawImp' nm

IForce : FC -> RawImp' nm -> RawImp' nm

IQuote : FC -> RawImp' nm -> RawImp' nm

IQuoteName : FC -> Name -> RawImp' nm

IQuoteDecl : FC -> List (ImpDecl' nm) -> RawImp' nm

IUnquote : FC -> RawImp' nm -> RawImp' nm

IRunElab : FC -> Bool -> RawImp' nm -> RawImp' nm

IPrimVal : FC -> Constant -> RawImp' nm

IType : FC -> RawImp' nm

IHole : FC -> String -> RawImp' nm

IUnifyLog : FC -> LogLevel -> RawImp' nm -> RawImp' nm

Implicit : FC -> Bool -> RawImp' nm

IWithUnambigNames : FC -> List (FC, Name) -> RawImp' nm -> RawImp' nm

Hints:

Functor RawImp'

Show nm => Show (RawImp' nm)

IFieldUpdate : Type

Visibility: public export

data IFieldUpdate' : Type -> Type

Totality: total
Visibility: public export
Constructors:

ISetField : List String -> RawImp' nm -> IFieldUpdate' nm

ISetFieldApp : List String -> RawImp' nm -> IFieldUpdate' nm

Hints:

Functor IFieldUpdate'

Show nm => Show (IFieldUpdate' nm)

AltType : Type

Visibility: public export

data AltType' : Type -> Type

Totality: total
Visibility: public export
Constructors:

FirstSuccess : AltType' nm

Unique : AltType' nm

UniqueDefault : RawImp' nm -> AltType' nm

Hint: 

Functor AltType'

FnOpt : Type

Visibility: public export

data FnOpt' : Type -> Type

Totality: total
Visibility: public export
Constructors:

Unsafe : FnOpt' nm

Inline : FnOpt' nm

NoInline : FnOpt' nm

Deprecate : FnOpt' nm

  Mark a function as deprecated.

TCInline : FnOpt' nm

Hint : Bool -> FnOpt' nm

GlobalHint : Bool -> FnOpt' nm

ExternFn : FnOpt' nm

ForeignFn : List (RawImp' nm) -> FnOpt' nm

ForeignExport : List (RawImp' nm) -> FnOpt' nm

Invertible : FnOpt' nm

Totality : TotalReq -> FnOpt' nm

Macro : FnOpt' nm

SpecArgs : List Name -> FnOpt' nm

Hints:

Functor FnOpt'

Show nm => Show (FnOpt' nm)

isTotalityReq : FnOpt' nm -> Bool

Visibility: public export

extractTotality : FnOpt' nm -> Maybe TotalReq

Visibility: export

findTotality : List (FnOpt' nm) -> Maybe TotalReq

Visibility: export

ImpTy : Type

Visibility: public export

ImpTy' : Type -> Type

Visibility: public export

ImpData : Type

Visibility: public export

data ImpData' : Type -> Type

Totality: total
Visibility: public export
Constructors:

MkImpData : FC -> Name -> Maybe (RawImp' nm) -> List DataOpt -> List (ImpTy' nm) -> ImpData' nm

MkImpLater : FC -> Name -> RawImp' nm -> ImpData' nm

Hints:

Functor ImpData'

Show nm => Show (ImpData' nm)

IField : Type

Visibility: public export

IField' : Type -> Type

Visibility: public export

ImpParameter : Type

Visibility: public export

ImpParameter' : Type -> Type

Visibility: public export

OldParameters' : Type -> Type

Visibility: public export

toOldParams : ImpParameter' (RawImp' nm) -> OldParameters' nm

Visibility: public export

fromOldParams : OldParameters' nm -> ImpParameter' (RawImp' nm)

Visibility: public export

0 ImpRecord : Type

Visibility: public export

0 DataHeader : Type -> Type

Visibility: public export

0 RecordBody : Type -> Type

Visibility: public export

record ImpRecordData : Type -> Type

  A record is defined by its header containing the name and parameters, and its body
  containing the constructor name, options, and a list of fields

Totality: total
Visibility: public export
Constructor: 

MkImpRecord : DataHeader nm -> RecordBody nm -> ImpRecordData nm

Projections:

.body : ImpRecordData nm -> RecordBody nm

.header : ImpRecordData nm -> DataHeader nm

Hints:

Functor ImpRecordData

Show nm => Show (ImpRecordData nm)

TTC (ImpRecordData Name)

.header : ImpRecordData nm -> DataHeader nm

Visibility: public export

header : ImpRecordData nm -> DataHeader nm

Visibility: public export

.body : ImpRecordData nm -> RecordBody nm

Visibility: public export

body : ImpRecordData nm -> RecordBody nm

Visibility: public export

data WithFlag : Type

Totality: total
Visibility: public export
Constructor: 

Syntactic : WithFlag

Hints:

Eq WithFlag

Reflect WithFlag

Reify WithFlag

ImpClause : Type

Visibility: public export

IImpClause : Type

Visibility: public export

data ImpClause' : Type -> Type

Totality: total
Visibility: public export
Constructors:

PatClause : FC -> RawImp' nm -> RawImp' nm -> ImpClause' nm

WithClause : FC -> RawImp' nm -> RigCount -> RawImp' nm -> Maybe (RigCount, Name) -> List WithFlag -> List (ImpClause' nm) -> ImpClause' nm

ImpossibleClause : FC -> RawImp' nm -> ImpClause' nm

Hints:

Functor ImpClause'

Show nm => Show (ImpClause' nm)

ImpDecl : Type

Visibility: public export

record IClaimData : Type -> Type

Totality: total
Visibility: public export
Constructor: 

MkIClaimData : RigCount -> Visibility -> List (FnOpt' nm) -> ImpTy' nm -> IClaimData nm

Projections:

.opts : IClaimData nm -> List (FnOpt' nm)

.rig : IClaimData nm -> RigCount

.type : IClaimData nm -> ImpTy' nm

.vis : IClaimData nm -> Visibility

Hints:

Functor IClaimData

Reflect (IClaimData Name)

Reify (IClaimData Name)

TTC (IClaimData Name)

.rig : IClaimData nm -> RigCount

Visibility: public export

rig : IClaimData nm -> RigCount

Visibility: public export

.vis : IClaimData nm -> Visibility

Visibility: public export

vis : IClaimData nm -> Visibility

Visibility: public export

.opts : IClaimData nm -> List (FnOpt' nm)

Visibility: public export

opts : IClaimData nm -> List (FnOpt' nm)

Visibility: public export

.type : IClaimData nm -> ImpTy' nm

Visibility: public export

type : IClaimData nm -> ImpTy' nm

Visibility: public export

data ImpDecl' : Type -> Type

Totality: total
Visibility: public export
Constructors:

IClaim : WithFC (IClaimData nm) -> ImpDecl' nm

IData : FC -> WithDefault Visibility Private -> Maybe TotalReq -> ImpData' nm -> ImpDecl' nm

IDef : FC -> Name -> List (ImpClause' nm) -> ImpDecl' nm

IParameters : FC -> List1 (ImpParameter' (RawImp' nm)) -> List (ImpDecl' nm) -> ImpDecl' nm

IRecord : FC -> Maybe String -> WithDefault Visibility Private -> Maybe TotalReq -> AddFC (ImpRecordData nm) -> ImpDecl' nm

IFail : FC -> Maybe String -> List (ImpDecl' nm) -> ImpDecl' nm

INamespace : FC -> Namespace -> List (ImpDecl' nm) -> ImpDecl' nm

ITransform : FC -> Name -> RawImp' nm -> RawImp' nm -> ImpDecl' nm

IRunElabDecl : FC -> RawImp' nm -> ImpDecl' nm

IPragma : FC -> List Name -> (NestedNames vars -> Env Term vars -> Core ()) -> ImpDecl' nm

ILog : Maybe (List String, Nat) -> ImpDecl' nm

IBuiltin : FC -> BuiltinType -> Name -> ImpDecl' nm

Hints:

Functor ImpDecl'

Show nm => Show (ImpDecl' nm)

mkWithClause : FC -> RawImp' nm -> List1 (RigCount, (RawImp' nm, Maybe (RigCount, Name))) -> List WithFlag -> List (ImpClause' nm) -> ImpClause' nm

Visibility: export

getFieldUpdateTerm : IFieldUpdate' nm -> RawImp' nm

Visibility: export

getFieldUpdatePath : IFieldUpdate' nm -> List String

Visibility: export

mapFieldUpdateTerm : (RawImp' nm -> RawImp' nm) -> IFieldUpdate' nm -> IFieldUpdate' nm

Visibility: export

isIPrimVal : RawImp' nm -> Maybe Constant

Visibility: export

data ImpREPL : Type

Totality: total
Visibility: public export
Constructors:

Eval : RawImp -> ImpREPL

Check : RawImp -> ImpREPL

ProofSearch : Name -> ImpREPL

ExprSearch : Name -> ImpREPL

GenerateDef : Int -> Name -> ImpREPL

Missing : Name -> ImpREPL

CheckTotal : Name -> ImpREPL

DebugInfo : Name -> ImpREPL

Quit : ImpREPL

mapAltType : (RawImp' nm -> RawImp' nm) -> AltType' nm -> AltType' nm

Visibility: export

lhsInCurrentNS : Ref Ctxt Defs => NestedNames vars -> RawImp -> Core RawImp

Visibility: export

findIBinds : RawImp' nm -> List String

Visibility: export

findImplicits : RawImp' nm -> List String

Visibility: export

implicitsAs : Ref Ctxt Defs => Int -> Defs -> List Name -> RawImp -> Core RawImp

Visibility: export

definedInBlock : Namespace -> List ImpDecl -> List Name

  `definedInBlock` is used to figure out which definitions should
  receive the additional arguments introduced by a Parameters directive

Visibility: export

isIVar : RawImp' nm -> Maybe (FC, nm)

Visibility: export

isIBindVar : RawImp' nm -> Maybe (FC, Name)

Visibility: export

getFC : RawImp' nm -> FC

Visibility: export

getFC : ImpDecl' nm -> FC

Visibility: public export

data Arg' : Type -> Type

Totality: total
Visibility: public export
Constructors:

Explicit : FC -> RawImp' nm -> Arg' nm

Auto : FC -> RawImp' nm -> Arg' nm

Named : FC -> Name -> RawImp' nm -> Arg' nm

Hint: 

Show nm => Show (Arg' nm)

Arg : Type

Visibility: public export

IArg : Type

Visibility: public export

isExplicit : Arg' nm -> Maybe (FC, RawImp' nm)

Visibility: export

unIArg : Arg' nm -> RawImp' nm

Visibility: export

getFnArgs : RawImp' nm -> List (Arg' nm) -> (RawImp' nm, List (Arg' nm))

Visibility: export

apply : RawImp' nm -> List (Arg' nm) -> RawImp' nm

Visibility: export

apply : RawImp' nm -> List (RawImp' nm) -> RawImp' nm

Visibility: export

gapply : RawImp' nm -> List (Maybe Name, RawImp' nm) -> RawImp' nm

Visibility: export

getFn : RawImp' nm -> RawImp' nm

Visibility: export

logRaw : Ref Ctxt Defs => LogTopic -> Nat -> Lazy String -> RawImp -> Core ()

Visibility: export