Mercurial > cpdt > repo

comparison src/Interps.v @ 292:2c88fc1dbe33

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A pass of double-quotes and LaTeX operator beautification
author Adam Chlipala <adam@chlipala.net>
date Wed, 10 Nov 2010 16:31:04 -0500
parents 05250878e4ca
children b441010125d4
comparison
equal deleted inserted replaced
291:da9ccc6bf572 292:2c88fc1dbe33
1 (* Copyright (c) 2008-2009, Adam Chlipala 1 (* Copyright (c) 2008-2010, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
62 62
63 (** The definitions that follow will be easier to read if we define some parsing notations for the constructors. *) 63 (** The definitions that follow will be easier to read if we define some parsing notations for the constructors. *)
64 64
65 Notation "# v" := (Var v) (at level 70). 65 Notation "# v" := (Var v) (at level 70).
66 66
67 (** printing ^ $\dag$ *)
67 Notation "^ n" := (Const n) (at level 70). 68 Notation "^ n" := (Const n) (at level 70).
69 (** printing +^ $\hat{+}$ *)
68 Infix "+^" := Plus (left associativity, at level 79). 70 Infix "+^" := Plus (left associativity, at level 79).
69 71
70 Infix "@" := App (left associativity, at level 77). 72 Infix "@" := App (left associativity, at level 77).
71 Notation "\ x , e" := (Abs (fun x => e)) (at level 78). 73 Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
72 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78). 74 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).