idris-1.3.1: Functional Programming Language with Dependent Types

LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell2010

Idris.ProofSearch

Description

 
Synopsis

Documentation

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

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

proofSearch Source #

Arguments

:: Bool

recursive search (False for refine)

-> 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 () 

resolveTC Source #

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).