Yi.Mode.Abella

Modes and utility function for working with the Abella interactive theorem prover.

Documentation

abellaModeEmacs :: TokenBasedMode Token

abella :: CommandArguments -> YiM BufferRef

Start Abella in a buffer

abellaEval :: YiM ()

abellaEvalFromProofPoint :: YiM ()

abellaUndo :: YiM ()

abellaGet :: YiM BufferRef

Return Abella's buffer; create it if necessary. Show it in another window.

abellaSend :: YiString -> YiM ()

Send a command to Abella