HERMIT.Monad

The HERMIT Monad

data HermitM a

runHM

embedHermitM

data HermitMEnv

data HermitMResult a

class LiftCoreM m

runTcM

runDsM

Saving Definitions

data RememberedName

type DefStash

saveDef

lookupDef

class HasStash m

Lemmas

data Equality

data LemmaName

data Lemma

type Lemmas

addLemma

Reader Information

class HasHermitMEnv m

mkEnv

getModGuts

class HasHscEnv m

Writer Information

class HasLemmas m

Messages

class HasDebugChan m

data DebugMessage

sendDebugMessage