| License | BSD3 |
|---|---|
| Maintainer | The Idris Community. |
| Safe Haskell | None |
| Language | Haskell2010 |
Idris.ProofSearch
Description
Synopsis
- 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
Arguments
| :: Bool | recursive search (False for |
| -> Bool | invoked from a tactic proof. If so, making new metavariables is meaningless, and there should be an error reported instead. |
| -> Bool | ambiguity ok |
| -> Bool | defer on failure |
| -> Int | maximum depth |
| -> (PTerm -> ElabD ()) | |
| -> Maybe Name | |
| -> Name | |
| -> [Name] | |
| -> [Name] | |
| -> IState | |
| -> ElabD () |
Arguments
| :: Bool | using default Int |
| -> Bool | allow open implementations |
| -> 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 interfaces. This will only pick up normal
implementations, never named implementations (which is enforced by
findImplementations).