idris-0.9.18.1: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.ProofSearch

Documentation

trivial :: (PTerm -> ElabD ()) -> IState -> ElabD () Source

trivialHoles :: [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD () Source

proofSearch :: Bool -> Bool -> Bool -> Bool -> Int -> (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] -> IState -> ElabD () Source