Idris.IdeSlave

Documentation

parseMessage :: String -> Either Err (SExp, Integer)

convSExp :: SExpable a => String -> a -> Integer -> String

data IdeSlaveCommand

Constructors

REPLCompletions String

Interpret String

TypeOf String

CaseSplit Int String

AddClause Int String

AddProofClause Int String

AddMissing Int String

MakeWithBlock Int String

ProofSearch Int String [String]

LoadFile String

Instances

Show IdeSlaveCommand

sexpToCommand :: SExp -> Maybe IdeSlaveCommand

data SExp

Constructors

SexpList [SExp]

StringAtom String

BoolAtom Bool

IntegerAtom Integer

SymbolAtom String

Instances

Eq SExp

Show SExp

SExpable SExp

class SExpable a where

Methods

toSExp :: a -> SExp

Instances

SExpable Bool

SExpable Int

SExpable Integer

SExpable String

SExpable Name

SExpable OutputAnnotation

SExpable NameOutput

SExpable SExp

SExpable a => SExpable [a]

SExpable a => SExpable (Maybe a)

(SExpable a, SExpable b) => SExpable (a, b)

(SExpable a, SExpable b, SExpable c) => SExpable (a, b, c)

(SExpable a, SExpable b, SExpable c, SExpable d) => SExpable (a, b, c, d)