On Thu, Mar 17, 2011 at 6:41 PM, wren ng thornton <[email protected]> wrote:
> On 3/17/11 5:12 PM, Conor McBride wrote: > >> On 17 Mar 2011, at 18:35, wren ng thornton wrote: >> >>> Another question on particulars. When dealing with natural numbers, we >>> run into the problem of defining subtraction. There are a few >>> reasonable definitions: >>> >> >> No there aren't. >> > > How about "pragmatically efficacious"? > If you must, you could always fall back on an encoding similar to the one that Brent used when introducing virtual species: http://byorgey.wordpress.com/2010/11/24/species-subtraction-made-simple/ along with some setoid that normalized for comparison on them, or you could just switch to type level Integers. -Edward > -- > Live well, > ~wren > > _______________________________________________ > Agda mailing list > [email protected] > https://lists.chalmers.se/mailman/listinfo/agda >
_______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
