idris-0.9.17: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.Prover

Documentation

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

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

proverSettings :: ElabState EState -> Settings Idris Source

assumptionNames :: ElabState EState -> [String] Source

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

elabStep :: ElabState EState -> ElabD a -> Idris (a, ElabState EState) Source

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

lifte :: ElabState EState -> ElabD a -> Idris a Source

receiveInput :: Handle -> ElabState EState -> Idris (Maybe String) Source

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