idris-0.9.15.1: Functional Programming Language with Dependent Types

Safe HaskellNone

Idris.Prover

Documentation

prover :: Bool -> Name -> Idris ()Source

showProof :: Bool -> Name -> [String] -> StringSource

proverSettings :: ElabState [PDecl] -> Settings IdrisSource

assumptionNames :: ElabState [PDecl] -> [String]Source

prove :: Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()Source

elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])Source

dumpState :: IState -> ProofState -> Idris ()Source

lifte :: ElabState [PDecl] -> ElabD a -> Idris aSource

receiveInput :: Handle -> ElabState [PDecl] -> Idris (Maybe String)Source

ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])Source