Idris.IDEMode.Holes

Definitions

record Premise : Type

Totality: total
Visibility: public export
Constructor: 

MkHolePremise : Name -> IPTerm -> RigCount -> Bool -> Premise

Projections:

.isImplicit : Premise -> Bool

.multiplicity : Premise -> RigCount

.name : Premise -> Name

.type : Premise -> IPTerm

Hints:

Pretty IdrisSyntax Premise

Show Premise

.name : Premise -> Name

Visibility: public export

name : Premise -> Name

Visibility: public export

.type : Premise -> IPTerm

Visibility: public export

type : Premise -> IPTerm

Visibility: public export

.multiplicity : Premise -> RigCount

Visibility: public export

multiplicity : Premise -> RigCount

Visibility: public export

.isImplicit : Premise -> Bool

Visibility: public export

isImplicit : Premise -> Bool

Visibility: public export

prettyRigHole : RigCount -> Doc IdrisSyntax

Visibility: export

record Data : Type

Totality: total
Visibility: public export
Constructor: 

MkHoleData : Name -> IPTerm -> List Premise -> Data

Projections:

.context : Data -> List Premise

.name : Data -> Name

.type : Data -> IPTerm

.name : Data -> Name

Visibility: public export

name : Data -> Name

Visibility: public export

.type : Data -> IPTerm

Visibility: public export

type : Data -> IPTerm

Visibility: public export

.context : Data -> List Premise

Visibility: public export

context : Data -> List Premise

Visibility: public export

prettyHoles : List Data -> Doc IdrisSyntax

Visibility: export

isHole : GlobalDef -> Maybe Nat

  If input is a hole, return number of locals in scope at binding
  point

Visibility: export

extractHoleData : Ref Ctxt Defs => Ref Syn SyntaxInfo => Defs -> Env Term vars -> Name -> Nat -> Term vars -> Core Data

Visibility: export

holeData : Ref Ctxt Defs => Ref Syn SyntaxInfo => Defs -> Env Term vars -> Name -> Nat -> Term vars -> Core Data

Visibility: export

getUserHolesData : Ref Ctxt Defs => Ref Syn SyntaxInfo => Core (List Data)

Visibility: export

showHole : Ref Ctxt Defs => Ref Syn SyntaxInfo => Defs -> Env Term vars -> Name -> Nat -> Term vars -> Core String

Visibility: export

prettyHole : Ref Ctxt Defs => Ref Syn SyntaxInfo => Defs -> Env Term vars -> Name -> Nat -> Term vars -> Core (Doc IdrisSyntax)

Visibility: export

holeIDE : Data -> HoleData

Visibility: export