| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
T2A.Tactics
- type Tactic = AgdaSignature -> Maybe (IO ())
- resolveTactic :: AgdaSignature -> [Tactic] -> IO ()
- resolveTacticGen :: AgdaSignature -> IO ()
- identity :: Tactic
Types
type Tactic = AgdaSignature -> Maybe (IO ())
A Tactic is a function that tries to give a corresponding
implementation to a Metis-generated proof step:
Given some Metis-generated Formulae
fof(a1, axiom, (a)). fof(normalize_0_2, plain, (a), inference(canonicalize, [], [a1])).
tstp2agda will generate the following signature for the function
fun-normalize-0-2 that given a1 return normalize_0_2
(Actually their corresponding formula)
fun-normalize-0-2 : {a : Set} → a → a
A Tactic is function that given a signature in the form of
AgdaSignature will determine the corresponding "implementation"
fun-normalize-0-2 : { a : Set} → a → a
fun-normalize-0-2 = id
Solvers
resolveTactic :: AgdaSignature -> [Tactic] -> IO ()
resolveTactic τ χ tries to find and implementation for τ
using every tactic in χ and in case of failure prints the default
implementation.
resolveTacticGen :: AgdaSignature -> IO ()
Similar to resolveTactic but using all the build-in tactics.