Safe Haskell | None |
---|---|

Language | Haskell2010 |

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