idris-0.9.17: Functional Programming Language with Dependent Types
Idris.ProofSearch
trivial :: (PTerm -> ElabD ()) -> IState -> ElabD () Source
proofSearch :: Bool -> Bool -> Bool -> Bool -> Int -> (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] -> IState -> ElabD () Source