| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Idris.ProofSearch
- trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()
- trivialHoles :: [Name] -> [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()
- proofSearch :: Bool -> Bool -> Bool -> Bool -> Int -> (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] -> [Name] -> IState -> ElabD ()
- resolveTC :: Bool -> Bool -> Int -> Term -> Name -> (PTerm -> ElabD ()) -> IState -> ElabD ()
Documentation
proofSearch :: Bool -> Bool -> Bool -> Bool -> Int -> (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] -> [Name] -> IState -> ElabD () 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).