[Agda] It feels like there isn't a way to do a partial subtraction nicely ... and a feature suggestion :)

[Ulf Norell]

On Mon, Mar 24, 2008 at 4:44 AM, Tristan Wibberley <tristan at wibberley.org>
wrote:

> On Sun, 2008-03-23 at 20:28 +0100, Ulf Norell wrote:
>
> > Defining True to be the record type with no fields is what's going to
> > make this possible. Records support eta equality, which means that any
> > record element "r" is equal to the record build by projecting the
> > fields of "r". In the case of True this means that any element of True
> > is equal to any other element of True. In particular, if the type
> > checker is trying to find something of type True there's only one
> > choice. Now, instead of defining NatLTE inductively you can define it
> > recursively:
> >
> > NatLTE : Nat -> Nat -> Set
> > NatLTE zero m = True
> > NatLTE (suc n) zero = False
> > NatLTE (suc n) (suc m) = NatLTE n m
> >
> > The type of minus is what you suggest:
> >
> > _-_ : (a : Nat) -> (b : Nat) -> {c : NatLTE b a} -> Nat
> > _-_ m zero = m
> > _-_ zero (suc _) {}  -- there can be no proof here
> > _-_ (suc n) (suc m) {p} = _-_ n m {p}
> >        -- a proof that suc n =< suc m is the same as a proof that n =<
> > m
>
> Do you mind if I add this to the documentation section of the wiki?
>
> I'll make a howto section to which other high-level templates can be
> added.
>

That would be great. Thanks.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080324/6b1d7c13/attachment.html