[Agda] Re: examples of tactics via reflection

[Nils Anders Danielsson]

On 2009-04-14 15:36, Dan Licata wrote:
> When A is weakenable with B, the type Check(canWeaken A B) computes
> definitionally to Unit, so there is no proof obligation.

It may be worth noticing that this works best when A and B are
(sufficiently) closed terms. As a concrete example, take the division
function from the standard library:

  _div_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → ℕ

As long as the divisor is of the form "suc n" the proof obligation is
discharged automatically, and because the unit type comes with
η-equality the hidden argument ≢0 does not need to be written out.

As another example, consider the conversion of a natural number to the
corresponding element of a finite set:

  #_ : ∀ m {n} {m<n : True (suc m ≤? n)} → Fin n

Here m has to be closed, and the initial part of n must consist of at
least m + 1 suc constructors.

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.