Protocol.IDE.Holes

Definitions

record HolePremise : Type

Totality: total
Visibility: public export
Constructor: 

MkHolePremise : String -> String -> HolePremise

Projections:

.name : HolePremise -> String

.type : HolePremise -> String

Hints:

FromSExpable HolePremise

SExpable HolePremise

.name : HolePremise -> String

Totality: total
Visibility: public export

name : HolePremise -> String

Totality: total
Visibility: public export

.type : HolePremise -> String

Totality: total
Visibility: public export

type : HolePremise -> String

Totality: total
Visibility: public export

record HoleData : Type

Totality: total
Visibility: public export
Constructor: 

MkHoleData : String -> String -> List HolePremise -> HoleData

Projections:

.context : HoleData -> List HolePremise

.name : HoleData -> String

.type : HoleData -> String

Hints:

FromSExpable HoleData

SExpable HoleData

.name : HoleData -> String

Totality: total
Visibility: public export

name : HoleData -> String

Totality: total
Visibility: public export

.type : HoleData -> String

Totality: total
Visibility: public export

type : HoleData -> String

Totality: total
Visibility: public export

.context : HoleData -> List HolePremise

Totality: total
Visibility: public export

context : HoleData -> List HolePremise

Totality: total
Visibility: public export