[Agda] dimly recalled strings?

[Nils Anders Danielsson]

On 2009-02-28 14:38, Conor McBride wrote:

> The library uses a postulate for the proof that equal strings are
> equal, but as things stand, that's gonna mess up computation.

Yes, I'm aware of this. Maybe the problem can be fixed if we add a
"BUILTIN" for equality and refl, and then use refl in the implementation
of primStringEquality. Have a look in the following modules:

  Agda.TypeChecking.Rules.Builtin
  Agda.TypeChecking.Monad.Builtin
  Agda.TypeChecking.Primitive

Patches are welcome, as always. You can also place an enhancement
request in the bug tracker, but our man-power is limited.

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