idris-0.9.20: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.ProofSearch

Synopsis

Documentation

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

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

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

resolveTC Source

Arguments

:: Bool

using default Int

-> Bool

allow metavariables in the goal

-> Int

depth

-> Term

top level goal, for error messages

-> Name

top level function name, to prevent loops

-> (PTerm -> ElabD ())

top level elaborator

-> IState 
-> ElabD () 

Resolve type classes. This will only pick up normal instances, never named instances (which is enforced by findInstances).