The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Hi all, I would like to know if hiding the
"match c with Ascii b0 b1 b2 b3 b4 b5 b6 b7 => … end"
when you do some "compute." or "simpl." with a module type wouldn't be
nicer (as I did in the joint file); the obvious disadvantage, is that
we can compute values only by rewritings, where the current version can
simply evaluate expressions; but we may gain the possibility to have
more readable code.

What do you do to keep types clean with ascii?

Attachment: char.v
Description: Binary data