[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

help with a typechecking error message

It looks like the only way the Prelude allows us to form expressions
that denote (already defined) characters is with the construction


where n is some natural below 128.  Is that right?  It would be nice if
there were single quote character terms--'A', 'a', 'B', 'b',... correlated
to strings in the expected way, so that, for example,

	char2stringA: lemma 'A' = seq("A")(0)

would be true.  I don't see any way of defining such expressions.

Mark Aronszajn
Reusable Software Research Group
West Virginia University