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 (* This file was automatically generated: do not edit *********************)
17 include "basic_1/A/defs.ma".
19 let rec lweight (a: A) on a: nat \def match a with [(ASort _ _) \Rightarrow O
20 | (AHead a1 a2) \Rightarrow (let TMP_1 \def (lweight a1) in (let TMP_2 \def
21 (lweight a2) in (let TMP_3 \def (plus TMP_1 TMP_2) in (S TMP_3))))].
26 \lambda (a1: A).(\lambda (a2: A).(let TMP_1 \def (lweight a1) in (let TMP_2
27 \def (lweight a2) in (lt TMP_1 TMP_2)))).