[Agda] Help with proofs

[Nils Anders Danielsson]

On Tue, May 6, 2008 at 12:52 AM, Tristan Wibberley
<tristan at wibberley.org> wrote:
>
>  It seems that the type of a proof object differs depending on the
>  definitions of the functions used to define its type

I am not quite sure I follow you, but you should note that Agda (and
similar systems like Epigram and Coq) implement the conversion rule,
which basically states that β(η)-equivalent things are
interchangeable.

If you want to define a function which does not evaluate, then you can
use the "abstract" keyword:

  abstract

    f : A -> B
    f x = rhs

When type checking things outside the scope of the abstract blocks in
the given module f will not evaluate. You can "force" the evaluation
of f yourself by defining and using a lemma:

  abstract

    f-eval : forall x -> f x ≡ rhs
    f-eval = ≡-refl

However, this will most likely be rather awkward and heavy-weight. If
you want to work like this, then I recommend some system with good
support for automation, like Coq or Isabelle.

-- 
/NAD