1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 notation < "mstyle mathsize big color #ff0000 background #0000ff scriptsizemultiplier 0.8 (x)"
16 non associative with precedence 50 for @{'red $x}.
18 definition red : ∀X:Type.∀t:X.X ≝ λT.λt.t.
19 interpretation "red" 'red x = (red _ x).
21 include "logic/equality.ma".
23 alias num (instance 0) = "natural number".
24 lemma foo : red ? 3 = 3.