Protocol.IDE.Result

Definitions

data OptionType : Type

Totality: total
Visibility: public export
Constructors:

BOOL : OptionType

STRING : OptionType

ATOM : OptionType

.sem : OptionType -> Type

Totality: total
Visibility: public export

record REPLOption : Type

Totality: total
Visibility: public export
Constructor: 

MkOption : String -> (type : OptionType) -> type .sem -> REPLOption

Projections:

.name : REPLOption -> String

.type : REPLOption -> OptionType

.val : ({rec:0} : REPLOption) -> (type {rec:0}) .sem

Hints:

Cast REPLOpt REPLOption

FromSExpable REPLOption

SExpable REPLOption

.name : REPLOption -> String

Totality: total
Visibility: public export

name : REPLOption -> String

Totality: total
Visibility: public export

.type : REPLOption -> OptionType

Totality: total
Visibility: public export

type : REPLOption -> OptionType

Totality: total
Visibility: public export

.val : ({rec:0} : REPLOption) -> (type {rec:0}) .sem

Totality: total
Visibility: public export

val : ({rec:0} : REPLOption) -> (type {rec:0}) .sem

Totality: total
Visibility: public export

record MetaVarLemma : Type

Totality: total
Visibility: public export
Constructor: 

MkMetaVarLemma : String -> String -> MetaVarLemma

Projections:

.application : MetaVarLemma -> String

.lemma : MetaVarLemma -> String

Hints:

FromSExpable MetaVarLemma

SExpable MetaVarLemma

.lemma : MetaVarLemma -> String

Totality: total
Visibility: public export

.application : MetaVarLemma -> String

Totality: total
Visibility: public export

lemma : MetaVarLemma -> String

Totality: total
Visibility: public export

application : MetaVarLemma -> String

Totality: total
Visibility: public export

record IdrisVersion : Type

Totality: total
Visibility: public export
Constructor: 

MkIdrisVersion : Nat -> Nat -> Nat -> Maybe String -> IdrisVersion

Projections:

.major : IdrisVersion -> Nat

.minor : IdrisVersion -> Nat

.patch : IdrisVersion -> Nat

.tag : IdrisVersion -> Maybe String

Hints:

FromSExpable IdrisVersion

SExpable IdrisVersion

.patch : IdrisVersion -> Nat

Totality: total
Visibility: public export

.minor : IdrisVersion -> Nat

Totality: total
Visibility: public export

.major : IdrisVersion -> Nat

Totality: total
Visibility: public export

patch : IdrisVersion -> Nat

Totality: total
Visibility: public export

minor : IdrisVersion -> Nat

Totality: total
Visibility: public export

major : IdrisVersion -> Nat

Totality: total
Visibility: public export

.tag : IdrisVersion -> Maybe String

Totality: total
Visibility: public export

tag : IdrisVersion -> Maybe String

Totality: total
Visibility: public export

data Result : Type

Totality: total
Visibility: public export
Constructors:

AString : String -> Result

AUnit : Result

AVersion : IdrisVersion -> Result

AMetaVarLemma : MetaVarLemma -> Result

ANameLocList : List (String, FileContext) -> Result

AHoleList : List HoleData -> Result

ACompletionList : List String -> String -> Result

ANameList : List String -> Result

AnOptionList : List REPLOption -> Result

AnIntroList : List1 String -> Result

Hints:

FromSExpable Result

SExpable Result