[Agda] Compile-time parsing

[Dan Licata]

On Dec15, Peter Thiemann wrote:
> Hi all,
> 
> I want to statically ensure that a string constant has a certain format.
> That is, I want an ill-formatted constant to be a typing error.
> 

Hi Peter,

Perhaps the use of "compile-time theorem proving" (see Sec 2.1.2) in
this paper:

http://www.cs.cmu.edu/~drl/pubs/ml10sectyp/ml10sectyp.pdf

might be helpful?  It's another example of the same technique that
others have suggested.

-Dan