string_of_source source ^
"record " ^ name ^ " " ^ pp_params pp_term params ^ ": " ^ pp_term ty ^
" \\def {" ^ pp_fields pp_term fields ^ "\n}"
- | Ast.LetRec (kind, definitions, (source, _, _)) ->
+ | Ast.LetRec (kind, definitions, (source, flavour, _)) ->
let rec get_guard i = function
| [] -> assert false (* Ast.Implicit `JustOne *)
| [term, _] when i = 1 -> term
(pp_term (get_guard i params))
(pp_term typ) (pp_term body)
in
- sprintf "%slet %s %s"
+ sprintf "%s%s %s %s"
(string_of_source source)
(match kind with `Inductive -> "rec" | `CoInductive -> "corec")
+ (NCicPp.string_of_flavour flavour)
(String.concat " and " (List.map map definitions))
let rec pp_value (status: #NCic.status) = function
include "basic_1/A/defs.ma".
-implied let rec A_rect (P: (A \to Type[0])) (f: (\forall (n: nat).(\forall
+implied rec lemma A_rect (P: (A \to Type[0])) (f: (\forall (n: nat).(\forall
(n0: nat).(P (ASort n n0))))) (f0: (\forall (a: A).((P a) \to (\forall (a0:
A).((P a0) \to (P (AHead a a0))))))) (a: A) on a: P a \def match a with
[(ASort n n0) \Rightarrow (f n n0) | (AHead a0 a1) \Rightarrow (f0 a0
| CSort: nat \to C
| CHead: C \to (K \to (T \to C)).
-let rec cweight (c: C) on c: nat \def match c with [(CSort _) \Rightarrow O |
-(CHead c0 _ t) \Rightarrow (plus (cweight c0) (tweight t))].
+rec definition cweight (c: C) on c: nat \def match c with [(CSort _)
+\Rightarrow O | (CHead c0 _ t) \Rightarrow (plus (cweight c0) (tweight t))].
definition clt:
C \to (C \to Prop)
\def
\lambda (c1: C).(\lambda (c2: C).(le (cweight c1) (cweight c2))).
-let rec CTail (k: K) (t: T) (c: C) on c: C \def match c with [(CSort n)
-\Rightarrow (CHead (CSort n) k t) | (CHead d h u) \Rightarrow (CHead (CTail k
-t d) h u)].
+rec definition CTail (k: K) (t: T) (c: C) on c: C \def match c with [(CSort
+n) \Rightarrow (CHead (CSort n) k t) | (CHead d h u) \Rightarrow (CHead
+(CTail k t d) h u)].
include "basic_1/C/defs.ma".
-implied let rec C_rect (P: (C \to Type[0])) (f: (\forall (n: nat).(P (CSort
+implied rec lemma C_rect (P: (C \to Type[0])) (f: (\forall (n: nat).(P (CSort
n)))) (f0: (\forall (c: C).((P c) \to (\forall (k: K).(\forall (t: T).(P
(CHead c k t))))))) (c: C) on c: P c \def match c with [(CSort n) \Rightarrow
(f n) | (CHead c0 k t) \Rightarrow (f0 c0 ((C_rect P f f0) c0) k t)].
| TLRef: nat \to T
| THead: K \to (T \to (T \to T)).
-let rec tweight (t: T) on t: nat \def match t with [(TSort _) \Rightarrow (S
-O) | (TLRef _) \Rightarrow (S O) | (THead _ u t0) \Rightarrow (S (plus
-(tweight u) (tweight t0)))].
+rec definition tweight (t: T) on t: nat \def match t with [(TSort _)
+\Rightarrow (S O) | (TLRef _) \Rightarrow (S O) | (THead _ u t0) \Rightarrow
+(S (plus (tweight u) (tweight t0)))].
definition tle:
T \to (T \to Prop)
include "basic_1/T/defs.ma".
-implied let rec T_rect (P: (T \to Type[0])) (f: (\forall (n: nat).(P (TSort
+implied rec lemma T_rect (P: (T \to Type[0])) (f: (\forall (n: nat).(P (TSort
n)))) (f0: (\forall (n: nat).(P (TLRef n)))) (f1: (\forall (k: K).(\forall
(t: T).((P t) \to (\forall (t0: T).((P t0) \to (P (THead k t t0)))))))) (t:
T) on t: P t \def match t with [(TSort n) \Rightarrow (f n) | (TLRef n)
include "basic_1/asucc/defs.ma".
-let rec aplus (g: G) (a: A) (n: nat) on n: A \def match n with [O \Rightarrow
-a | (S n0) \Rightarrow (asucc g (aplus g a n0))].
+rec definition aplus (g: G) (a: A) (n: nat) on n: A \def match n with [O
+\Rightarrow a | (S n0) \Rightarrow (asucc g (aplus g a n0))].
include "basic_1/C/defs.ma".
-let rec cbk (c: C) on c: nat \def match c with [(CSort m) \Rightarrow m |
-(CHead c0 _ _) \Rightarrow (cbk c0)].
+rec definition cbk (c: C) on c: nat \def match c with [(CSort m) \Rightarrow
+m | (CHead c0 _ _) \Rightarrow (cbk c0)].
-let rec app1 (c: C) on c: T \to T \def \lambda (t: T).(match c with [(CSort
-_) \Rightarrow t | (CHead c0 k u) \Rightarrow (app1 c0 (THead k u t))]).
+rec definition app1 (c: C) on c: T \to T \def \lambda (t: T).(match c with
+[(CSort _) \Rightarrow t | (CHead c0 k u) \Rightarrow (app1 c0 (THead k u
+t))]).
include "basic_1/aprem/defs.ma".
-implied let rec aprem_ind (P: (nat \to (A \to (A \to Prop)))) (f: (\forall
+implied rec lemma aprem_ind (P: (nat \to (A \to (A \to Prop)))) (f: (\forall
(a1: A).(\forall (a2: A).(P O (AHead a1 a2) a1)))) (f0: (\forall (a2:
A).(\forall (a: A).(\forall (i: nat).((aprem i a2 a) \to ((P i a2 a) \to
(\forall (a1: A).(P (S i) (AHead a1 a2) a)))))))) (n: nat) (a: A) (a0: A)
include "basic_1/getl/drop.ma".
-implied let rec arity_ind (g: G) (P: (C \to (T \to (A \to Prop)))) (f:
+implied rec lemma arity_ind (g: G) (P: (C \to (T \to (A \to Prop)))) (f:
(\forall (c: C).(\forall (n: nat).(P c (TSort n) (ASort O n))))) (f0:
(\forall (c: C).(\forall (d: C).(\forall (u: T).(\forall (i: nat).((getl i c
(CHead d (Bind Abbr) u)) \to (\forall (a: A).((arity g d u a) \to ((P d u a)
include "basic_1/G/defs.ma".
-let rec asucc (g: G) (l: A) on l: A \def match l with [(ASort n0 n)
+rec definition asucc (g: G) (l: A) on l: A \def match l with [(ASort n0 n)
\Rightarrow (match n0 with [O \Rightarrow (ASort O (next g n)) | (S h)
\Rightarrow (ASort h n)]) | (AHead a1 a2) \Rightarrow (AHead a1 (asucc g
a2))].
include "basic_1/C/fwd.ma".
-implied let rec clear_ind (P: (C \to (C \to Prop))) (f: (\forall (b:
+implied rec lemma clear_ind (P: (C \to (C \to Prop))) (f: (\forall (b:
B).(\forall (e: C).(\forall (u: T).(P (CHead e (Bind b) u) (CHead e (Bind b)
u)))))) (f0: (\forall (e: C).(\forall (c: C).((clear e c) \to ((P e c) \to
(\forall (f0: F).(\forall (u: T).(P (CHead e (Flat f0) u) c)))))))) (c: C)
include "basic_1/s/defs.ma".
-let rec clen (c: C) on c: nat \def match c with [(CSort _) \Rightarrow O |
-(CHead c0 k _) \Rightarrow (s k (clen c0))].
+rec definition clen (c: C) on c: nat \def match c with [(CSort _) \Rightarrow
+O | (CHead c0 k _) \Rightarrow (s k (clen c0))].
include "basic_1/cnt/defs.ma".
-implied let rec cnt_ind (P: (T \to Prop)) (f: (\forall (n: nat).(P (TSort
+implied rec lemma cnt_ind (P: (T \to Prop)) (f: (\forall (n: nat).(P (TSort
n)))) (f0: (\forall (t: T).((cnt t) \to ((P t) \to (\forall (k: K).(\forall
(v: T).(P (THead k v t)))))))) (t: T) (c: cnt t) on c: P t \def match c with
[(cnt_sort n) \Rightarrow (f n) | (cnt_head t0 c0 k v) \Rightarrow (f0 t0 c0
include "basic_1/csuba/defs.ma".
-implied let rec csuba_ind (g: G) (P: (C \to (C \to Prop))) (f: (\forall (n:
+implied rec lemma csuba_ind (g: G) (P: (C \to (C \to Prop))) (f: (\forall (n:
nat).(P (CSort n) (CSort n)))) (f0: (\forall (c1: C).(\forall (c2: C).((csuba
g c1 c2) \to ((P c1 c2) \to (\forall (k: K).(\forall (u: T).(P (CHead c1 k u)
(CHead c2 k u))))))))) (f1: (\forall (c1: C).(\forall (c2: C).((csuba g c1
include "basic_1/csubc/defs.ma".
-implied let rec csubc_ind (g: G) (P: (C \to (C \to Prop))) (f: (\forall (n:
+implied rec lemma csubc_ind (g: G) (P: (C \to (C \to Prop))) (f: (\forall (n:
nat).(P (CSort n) (CSort n)))) (f0: (\forall (c1: C).(\forall (c2: C).((csubc
g c1 c2) \to ((P c1 c2) \to (\forall (k: K).(\forall (v: T).(P (CHead c1 k v)
(CHead c2 k v))))))))) (f1: (\forall (c1: C).(\forall (c2: C).((csubc g c1
include "basic_1/C/fwd.ma".
-implied let rec csubst0_ind (P: (nat \to (T \to (C \to (C \to Prop))))) (f:
+implied rec lemma csubst0_ind (P: (nat \to (T \to (C \to (C \to Prop))))) (f:
(\forall (k: K).(\forall (i: nat).(\forall (v: T).(\forall (u1: T).(\forall
(u2: T).((subst0 i v u1 u2) \to (\forall (c: C).(P (s k i) v (CHead c k u1)
(CHead c k u2)))))))))) (f0: (\forall (k: K).(\forall (i: nat).(\forall (c1:
include "basic_1/csubt/defs.ma".
-implied let rec csubt_ind (g: G) (P: (C \to (C \to Prop))) (f: (\forall (n:
+implied rec lemma csubt_ind (g: G) (P: (C \to (C \to Prop))) (f: (\forall (n:
nat).(P (CSort n) (CSort n)))) (f0: (\forall (c1: C).(\forall (c2: C).((csubt
g c1 c2) \to ((P c1 c2) \to (\forall (k: K).(\forall (u: T).(P (CHead c1 k u)
(CHead c2 k u))))))))) (f1: (\forall (c1: C).(\forall (c2: C).((csubt g c1
include "basic_1/csubv/defs.ma".
-implied let rec csubv_ind (P: (C \to (C \to Prop))) (f: (\forall (n: nat).(P
-(CSort n) (CSort n)))) (f0: (\forall (c1: C).(\forall (c2: C).((csubv c1 c2)
-\to ((P c1 c2) \to (\forall (v1: T).(\forall (v2: T).(P (CHead c1 (Bind Void)
-v1) (CHead c2 (Bind Void) v2))))))))) (f1: (\forall (c1: C).(\forall (c2:
-C).((csubv c1 c2) \to ((P c1 c2) \to (\forall (b1: B).((not (eq B b1 Void))
-\to (\forall (b2: B).(\forall (v1: T).(\forall (v2: T).(P (CHead c1 (Bind b1)
-v1) (CHead c2 (Bind b2) v2)))))))))))) (f2: (\forall (c1: C).(\forall (c2:
-C).((csubv c1 c2) \to ((P c1 c2) \to (\forall (f2: F).(\forall (f3:
-F).(\forall (v1: T).(\forall (v2: T).(P (CHead c1 (Flat f2) v1) (CHead c2
-(Flat f3) v2))))))))))) (c: C) (c0: C) (c1: csubv c c0) on c1: P c c0 \def
-match c1 with [(csubv_sort n) \Rightarrow (f n) | (csubv_void c2 c3 c4 v1 v2)
-\Rightarrow (f0 c2 c3 c4 ((csubv_ind P f f0 f1 f2) c2 c3 c4) v1 v2) |
-(csubv_bind c2 c3 c4 b1 n b2 v1 v2) \Rightarrow (f1 c2 c3 c4 ((csubv_ind P f
-f0 f1 f2) c2 c3 c4) b1 n b2 v1 v2) | (csubv_flat c2 c3 c4 f3 f4 v1 v2)
-\Rightarrow (f2 c2 c3 c4 ((csubv_ind P f f0 f1 f2) c2 c3 c4) f3 f4 v1 v2)].
+implied rec lemma csubv_ind (P: (C \to (C \to Prop))) (f: (\forall (n:
+nat).(P (CSort n) (CSort n)))) (f0: (\forall (c1: C).(\forall (c2: C).((csubv
+c1 c2) \to ((P c1 c2) \to (\forall (v1: T).(\forall (v2: T).(P (CHead c1
+(Bind Void) v1) (CHead c2 (Bind Void) v2))))))))) (f1: (\forall (c1:
+C).(\forall (c2: C).((csubv c1 c2) \to ((P c1 c2) \to (\forall (b1: B).((not
+(eq B b1 Void)) \to (\forall (b2: B).(\forall (v1: T).(\forall (v2: T).(P
+(CHead c1 (Bind b1) v1) (CHead c2 (Bind b2) v2)))))))))))) (f2: (\forall (c1:
+C).(\forall (c2: C).((csubv c1 c2) \to ((P c1 c2) \to (\forall (f2:
+F).(\forall (f3: F).(\forall (v1: T).(\forall (v2: T).(P (CHead c1 (Flat f2)
+v1) (CHead c2 (Flat f3) v2))))))))))) (c: C) (c0: C) (c1: csubv c c0) on c1:
+P c c0 \def match c1 with [(csubv_sort n) \Rightarrow (f n) | (csubv_void c2
+c3 c4 v1 v2) \Rightarrow (f0 c2 c3 c4 ((csubv_ind P f f0 f1 f2) c2 c3 c4) v1
+v2) | (csubv_bind c2 c3 c4 b1 n b2 v1 v2) \Rightarrow (f1 c2 c3 c4
+((csubv_ind P f f0 f1 f2) c2 c3 c4) b1 n b2 v1 v2) | (csubv_flat c2 c3 c4 f3
+f4 v1 v2) \Rightarrow (f2 c2 c3 c4 ((csubv_ind P f f0 f1 f2) c2 c3 c4) f3 f4
+v1 v2)].
include "basic_1/C/fwd.ma".
-implied let rec drop_ind (P: (nat \to (nat \to (C \to (C \to Prop))))) (f:
+implied rec lemma drop_ind (P: (nat \to (nat \to (C \to (C \to Prop))))) (f:
(\forall (c: C).(P O O c c))) (f0: (\forall (k: K).(\forall (h: nat).(\forall
(c: C).(\forall (e: C).((drop (r k h) O c e) \to ((P (r k h) O c e) \to
(\forall (u: T).(P (S h) O (CHead c k u) e))))))))) (f1: (\forall (k:
nat).((drop h d c1 c2) \to (\forall (c3: C).(\forall (hds: PList).((drop1 hds
c2 c3) \to (drop1 (PCons h d hds) c1 c3)))))))).
-let rec ptrans (hds: PList) on hds: nat \to PList \def \lambda (i:
+rec definition ptrans (hds: PList) on hds: nat \to PList \def \lambda (i:
nat).(match hds with [PNil \Rightarrow PNil | (PCons h d hds0) \Rightarrow
(let j \def (trans hds0 i) in (let q \def (ptrans hds0 i) in (match (blt j d)
with [true \Rightarrow (PCons h (minus d (S j)) q) | false \Rightarrow
include "basic_1/drop1/defs.ma".
-implied let rec drop1_ind (P: (PList \to (C \to (C \to Prop)))) (f: (\forall
-(c: C).(P PNil c c))) (f0: (\forall (c1: C).(\forall (c2: C).(\forall (h:
-nat).(\forall (d: nat).((drop h d c1 c2) \to (\forall (c3: C).(\forall (hds:
-PList).((drop1 hds c2 c3) \to ((P hds c2 c3) \to (P (PCons h d hds) c1
-c3))))))))))) (p: PList) (c: C) (c0: C) (d: drop1 p c c0) on d: P p c c0 \def
-match d with [(drop1_nil c1) \Rightarrow (f c1) | (drop1_cons c1 c2 h d0 d1
-c3 hds d2) \Rightarrow (f0 c1 c2 h d0 d1 c3 hds d2 ((drop1_ind P f f0) hds c2
-c3 d2))].
+implied rec lemma drop1_ind (P: (PList \to (C \to (C \to Prop)))) (f:
+(\forall (c: C).(P PNil c c))) (f0: (\forall (c1: C).(\forall (c2:
+C).(\forall (h: nat).(\forall (d: nat).((drop h d c1 c2) \to (\forall (c3:
+C).(\forall (hds: PList).((drop1 hds c2 c3) \to ((P hds c2 c3) \to (P (PCons
+h d hds) c1 c3))))))))))) (p: PList) (c: C) (c0: C) (d: drop1 p c c0) on d: P
+p c c0 \def match d with [(drop1_nil c1) \Rightarrow (f c1) | (drop1_cons c1
+c2 h d0 d1 c3 hds d2) \Rightarrow (f0 c1 c2 h d0 d1 c3 hds d2 ((drop1_ind P f
+f0) hds c2 c3 d2))].
lemma drop1_gen_pnil:
\forall (c1: C).(\forall (c2: C).((drop1 PNil c1 c2) \to (eq C c1 c2)))
include "basic_1/ex0/defs.ma".
-implied let rec leqz_ind (P: (A \to (A \to Prop))) (f: (\forall (h1:
+implied rec lemma leqz_ind (P: (A \to (A \to Prop))) (f: (\forall (h1:
nat).(\forall (h2: nat).(\forall (n1: nat).(\forall (n2: nat).((eq nat (plus
h1 n2) (plus h2 n1)) \to (P (ASort h1 n1) (ASort h2 n2)))))))) (f0: (\forall
(a1: A).(\forall (a2: A).((leqz a1 a2) \to ((P a1 a2) \to (\forall (a3:
include "basic_1/leq/defs.ma".
-implied let rec leq_ind (g: G) (P: (A \to (A \to Prop))) (f: (\forall (h1:
+implied rec lemma leq_ind (g: G) (P: (A \to (A \to Prop))) (f: (\forall (h1:
nat).(\forall (h2: nat).(\forall (n1: nat).(\forall (n2: nat).(\forall (k:
nat).((eq A (aplus g (ASort h1 n1) k) (aplus g (ASort h2 n2) k)) \to (P
(ASort h1 n1) (ASort h2 n2))))))))) (f0: (\forall (a1: A).(\forall (a2:
include "basic_1/s/defs.ma".
-let rec lref_map (f: (nat \to nat)) (d: nat) (t: T) on t: T \def match t with
-[(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i
-d) with [true \Rightarrow i | false \Rightarrow (f i)])) | (THead k u t0)
-\Rightarrow (THead k (lref_map f d u) (lref_map f (s k d) t0))].
+rec definition lref_map (f: (nat \to nat)) (d: nat) (t: T) on t: T \def match
+t with [(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match
+(blt i d) with [true \Rightarrow i | false \Rightarrow (f i)])) | (THead k u
+t0) \Rightarrow (THead k (lref_map f d u) (lref_map f (s k d) t0))].
definition lift:
nat \to (nat \to (T \to T))
\lambda (h: nat).(\lambda (i: nat).(\lambda (t: T).(lref_map (\lambda (x:
nat).(plus x h)) i t))).
-let rec lifts (h: nat) (d: nat) (ts: TList) on ts: TList \def match ts with
-[TNil \Rightarrow TNil | (TCons t ts0) \Rightarrow (TCons (lift h d t) (lifts
-h d ts0))].
+rec definition lifts (h: nat) (d: nat) (ts: TList) on ts: TList \def match ts
+with [TNil \Rightarrow TNil | (TCons t ts0) \Rightarrow (TCons (lift h d t)
+(lifts h d ts0))].
include "basic_1/lift/defs.ma".
-let rec trans (hds: PList) on hds: nat \to nat \def \lambda (i: nat).(match
-hds with [PNil \Rightarrow i | (PCons h d hds0) \Rightarrow (let j \def
-(trans hds0 i) in (match (blt j d) with [true \Rightarrow j | false
+rec definition trans (hds: PList) on hds: nat \to nat \def \lambda (i:
+nat).(match hds with [PNil \Rightarrow i | (PCons h d hds0) \Rightarrow (let
+j \def (trans hds0 i) in (match (blt j d) with [true \Rightarrow j | false
\Rightarrow (plus j h)]))]).
-let rec lift1 (hds: PList) on hds: T \to T \def \lambda (t: T).(match hds
-with [PNil \Rightarrow t | (PCons h d hds0) \Rightarrow (lift h d (lift1 hds0
-t))]).
+rec definition lift1 (hds: PList) on hds: T \to T \def \lambda (t: T).(match
+hds with [PNil \Rightarrow t | (PCons h d hds0) \Rightarrow (lift h d (lift1
+hds0 t))]).
-let rec lifts1 (hds: PList) (ts: TList) on ts: TList \def match ts with [TNil
-\Rightarrow TNil | (TCons t ts0) \Rightarrow (TCons (lift1 hds t) (lifts1 hds
-ts0))].
+rec definition lifts1 (hds: PList) (ts: TList) on ts: TList \def match ts
+with [TNil \Rightarrow TNil | (TCons t ts0) \Rightarrow (TCons (lift1 hds t)
+(lifts1 hds ts0))].
include "basic_1/A/defs.ma".
-let rec lweight (a: A) on a: nat \def match a with [(ASort _ _) \Rightarrow O
-| (AHead a1 a2) \Rightarrow (S (plus (lweight a1) (lweight a2)))].
+rec definition lweight (a: A) on a: nat \def match a with [(ASort _ _)
+\Rightarrow O | (AHead a1 a2) \Rightarrow (S (plus (lweight a1) (lweight
+a2)))].
definition llt:
A \to (A \to Prop)
include "basic_1/G/defs.ma".
-let rec next_plus (g: G) (n: nat) (i: nat) on i: nat \def match i with [O
-\Rightarrow n | (S i0) \Rightarrow (next g (next_plus g n i0))].
+rec definition next_plus (g: G) (n: nat) (i: nat) on i: nat \def match i with
+[O \Rightarrow n | (S i0) \Rightarrow (next g (next_plus g n i0))].
\lambda (c: C).(\lambda (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (eq T t1
t2)))).
-let rec nfs2 (c: C) (ts: TList) on ts: Prop \def match ts with [TNil
+rec definition nfs2 (c: C) (ts: TList) on ts: Prop \def match ts with [TNil
\Rightarrow True | (TCons t ts0) \Rightarrow (land (nf2 c t) (nfs2 c ts0))].
include "basic_1/pc3/props.ma".
-implied let rec pc3_left_ind (c: C) (P: (T \to (T \to Prop))) (f: (\forall
+implied rec lemma pc3_left_ind (c: C) (P: (T \to (T \to Prop))) (f: (\forall
(t: T).(P t t))) (f0: (\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to
(\forall (t3: T).((pc3_left c t2 t3) \to ((P t2 t3) \to (P t1 t3)))))))) (f1:
(\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (\forall (t3:
include "basic_1/subst0/fwd.ma".
-implied let rec pr0_ind (P: (T \to (T \to Prop))) (f: (\forall (t: T).(P t
+implied rec lemma pr0_ind (P: (T \to (T \to Prop))) (f: (\forall (t: T).(P t
t))) (f0: (\forall (u1: T).(\forall (u2: T).((pr0 u1 u2) \to ((P u1 u2) \to
(\forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to ((P t1 t2) \to (\forall
(k: K).(P (THead k u1 t1) (THead k u2 t2)))))))))))) (f1: (\forall (u:
include "basic_1/pr1/defs.ma".
-implied let rec pr1_ind (P: (T \to (T \to Prop))) (f: (\forall (t: T).(P t
+implied rec lemma pr1_ind (P: (T \to (T \to Prop))) (f: (\forall (t: T).(P t
t))) (f0: (\forall (t2: T).(\forall (t1: T).((pr0 t1 t2) \to (\forall (t3:
T).((pr1 t2 t3) \to ((P t2 t3) \to (P t1 t3)))))))) (t: T) (t0: T) (p: pr1 t
t0) on p: P t t0 \def match p with [(pr1_refl t1) \Rightarrow (f t1) |
include "basic_1/pr2/fwd.ma".
-implied let rec pr3_ind (c: C) (P: (T \to (T \to Prop))) (f: (\forall (t:
+implied rec lemma pr3_ind (c: C) (P: (T \to (T \to Prop))) (f: (\forall (t:
T).(P t t))) (f0: (\forall (t2: T).(\forall (t1: T).((pr2 c t1 t2) \to
(\forall (t3: T).((pr3 c t2 t3) \to ((P t2 t3) \to (P t1 t3)))))))) (t: T)
(t0: T) (p: pr3 c t t0) on p: P t t0 \def match p with [(pr3_refl t1)
include "basic_1/drop1/defs.ma".
-let rec sc3 (g: G) (a: A) on a: C \to (T \to Prop) \def \lambda (c:
+rec definition sc3 (g: G) (a: A) on a: C \to (T \to Prop) \def \lambda (c:
C).(\lambda (t: T).(match a with [(ASort h n) \Rightarrow (land (arity g c t
(ASort h n)) (sn3 c t)) | (AHead a1 a2) \Rightarrow (land (arity g c t (AHead
a1 a2)) (\forall (d: C).(\forall (w: T).((sc3 g a1 d w) \to (\forall (is:
| sn3_sing: \forall (t1: T).(((\forall (t2: T).((((eq T t1 t2) \to (\forall
(P: Prop).P))) \to ((pr3 c t1 t2) \to (sn3 c t2))))) \to (sn3 c t1)).
-let rec sns3 (c: C) (ts: TList) on ts: Prop \def match ts with [TNil
+rec definition sns3 (c: C) (ts: TList) on ts: Prop \def match ts with [TNil
\Rightarrow True | (TCons t ts0) \Rightarrow (land (sn3 c t) (sns3 c ts0))].
include "basic_1/pr3/props.ma".
-implied let rec sn3_ind (c: C) (P: (T \to Prop)) (f: (\forall (t1:
+implied rec lemma sn3_ind (c: C) (P: (T \to Prop)) (f: (\forall (t1:
T).(((\forall (t2: T).((((eq T t1 t2) \to (\forall (P0: Prop).P0))) \to ((pr3
c t1 t2) \to (sn3 c t2))))) \to (((\forall (t2: T).((((eq T t1 t2) \to
(\forall (P0: Prop).P0))) \to ((pr3 c t1 t2) \to (P t2))))) \to (P t1)))))
include "basic_1/sty0/defs.ma".
-implied let rec sty0_ind (g: G) (P: (C \to (T \to (T \to Prop)))) (f:
+implied rec lemma sty0_ind (g: G) (P: (C \to (T \to (T \to Prop)))) (f:
(\forall (c: C).(\forall (n: nat).(P c (TSort n) (TSort (next g n)))))) (f0:
(\forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c
(CHead d (Bind Abbr) v)) \to (\forall (w: T).((sty0 g d v w) \to ((P d v w)
include "basic_1/sty1/defs.ma".
-implied let rec sty1_ind (g: G) (c: C) (t1: T) (P: (T \to Prop)) (f: (\forall
-(t2: T).((sty0 g c t1 t2) \to (P t2)))) (f0: (\forall (t: T).((sty1 g c t1 t)
-\to ((P t) \to (\forall (t2: T).((sty0 g c t t2) \to (P t2))))))) (t: T) (s0:
-sty1 g c t1 t) on s0: P t \def match s0 with [(sty1_sty0 t2 s1) \Rightarrow
-(f t2 s1) | (sty1_sing t0 s1 t2 s2) \Rightarrow (f0 t0 s1 ((sty1_ind g c t1 P
-f f0) t0 s1) t2 s2)].
+implied rec lemma sty1_ind (g: G) (c: C) (t1: T) (P: (T \to Prop)) (f:
+(\forall (t2: T).((sty0 g c t1 t2) \to (P t2)))) (f0: (\forall (t: T).((sty1
+g c t1 t) \to ((P t) \to (\forall (t2: T).((sty0 g c t t2) \to (P t2)))))))
+(t: T) (s0: sty1 g c t1 t) on s0: P t \def match s0 with [(sty1_sty0 t2 s1)
+\Rightarrow (f t2 s1) | (sty1_sing t0 s1 t2 s2) \Rightarrow (f0 t0 s1
+((sty1_ind g c t1 P f f0) t0 s1) t2 s2)].
include "basic_1/lift/defs.ma".
-let rec subst (d: nat) (v: T) (t: T) on t: T \def match t with [(TSort n)
-\Rightarrow (TSort n) | (TLRef i) \Rightarrow (match (blt i d) with [true
+rec definition subst (d: nat) (v: T) (t: T) on t: T \def match t with [(TSort
+n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (match (blt i d) with [true
\Rightarrow (TLRef i) | false \Rightarrow (match (blt d i) with [true
\Rightarrow (TLRef (pred i)) | false \Rightarrow (lift d O v)])]) | (THead k
u t0) \Rightarrow (THead k (subst d v u) (subst (s k d) v t0))].
include "basic_1/lift/fwd.ma".
-implied let rec subst0_ind (P: (nat \to (T \to (T \to (T \to Prop))))) (f:
+implied rec lemma subst0_ind (P: (nat \to (T \to (T \to (T \to Prop))))) (f:
(\forall (v: T).(\forall (i: nat).(P i v (TLRef i) (lift (S i) O v))))) (f0:
(\forall (v: T).(\forall (u2: T).(\forall (u1: T).(\forall (i: nat).((subst0
i v u1 u2) \to ((P i v u1 u2) \to (\forall (t: T).(\forall (k: K).(P i v
| TNil: TList
| TCons: T \to (TList \to TList).
-let rec THeads (k: K) (us: TList) on us: T \to T \def \lambda (t: T).(match
-us with [TNil \Rightarrow t | (TCons u ul) \Rightarrow (THead k u (THeads k
-ul t))]).
+rec definition THeads (k: K) (us: TList) on us: T \to T \def \lambda (t:
+T).(match us with [TNil \Rightarrow t | (TCons u ul) \Rightarrow (THead k u
+(THeads k ul t))]).
-let rec TApp (ts: TList) on ts: T \to TList \def \lambda (v: T).(match ts
-with [TNil \Rightarrow (TCons v TNil) | (TCons t ts0) \Rightarrow (TCons t
+rec definition TApp (ts: TList) on ts: T \to TList \def \lambda (v: T).(match
+ts with [TNil \Rightarrow (TCons v TNil) | (TCons t ts0) \Rightarrow (TCons t
(TApp ts0 v))]).
-let rec tslen (ts: TList) on ts: nat \def match ts with [TNil \Rightarrow O |
-(TCons _ ts0) \Rightarrow (S (tslen ts0))].
+rec definition tslen (ts: TList) on ts: nat \def match ts with [TNil
+\Rightarrow O | (TCons _ ts0) \Rightarrow (S (tslen ts0))].
definition tslt:
TList \to (TList \to Prop)
\lambda (f: ((nat \to nat))).(\lambda (w: nat).(\lambda (n: nat).(match n
with [O \Rightarrow w | (S m) \Rightarrow (f m)]))).
-let rec weight_map (f: (nat \to nat)) (t: T) on t: nat \def match t with
-[(TSort _) \Rightarrow O | (TLRef n) \Rightarrow (f n) | (THead k u t0)
+rec definition weight_map (f: (nat \to nat)) (t: T) on t: nat \def match t
+with [(TSort _) \Rightarrow O | (TLRef n) \Rightarrow (f n) | (THead k u t0)
\Rightarrow (match k with [(Bind b) \Rightarrow (match b with [Abbr
\Rightarrow (S (plus (weight_map f u) (weight_map (wadd f (S (weight_map f
u))) t0))) | Abst \Rightarrow (S (plus (weight_map f u) (weight_map (wadd f
include "basic_1/pc3/props.ma".
-implied let rec ty3_ind (g: G) (P: (C \to (T \to (T \to Prop)))) (f: (\forall
-(c: C).(\forall (t2: T).(\forall (t: T).((ty3 g c t2 t) \to ((P c t2 t) \to
-(\forall (u: T).(\forall (t1: T).((ty3 g c u t1) \to ((P c u t1) \to ((pc3 c
-t1 t2) \to (P c u t2)))))))))))) (f0: (\forall (c: C).(\forall (m: nat).(P c
-(TSort m) (TSort (next g m)))))) (f1: (\forall (n: nat).(\forall (c:
-C).(\forall (d: C).(\forall (u: T).((getl n c (CHead d (Bind Abbr) u)) \to
-(\forall (t: T).((ty3 g d u t) \to ((P d u t) \to (P c (TLRef n) (lift (S n)
-O t))))))))))) (f2: (\forall (n: nat).(\forall (c: C).(\forall (d:
+implied rec lemma ty3_ind (g: G) (P: (C \to (T \to (T \to Prop)))) (f:
+(\forall (c: C).(\forall (t2: T).(\forall (t: T).((ty3 g c t2 t) \to ((P c t2
+t) \to (\forall (u: T).(\forall (t1: T).((ty3 g c u t1) \to ((P c u t1) \to
+((pc3 c t1 t2) \to (P c u t2)))))))))))) (f0: (\forall (c: C).(\forall (m:
+nat).(P c (TSort m) (TSort (next g m)))))) (f1: (\forall (n: nat).(\forall
+(c: C).(\forall (d: C).(\forall (u: T).((getl n c (CHead d (Bind Abbr) u))
+\to (\forall (t: T).((ty3 g d u t) \to ((P d u t) \to (P c (TLRef n) (lift (S
+n) O t))))))))))) (f2: (\forall (n: nat).(\forall (c: C).(\forall (d:
C).(\forall (u: T).((getl n c (CHead d (Bind Abst) u)) \to (\forall (t:
T).((ty3 g d u t) \to ((P d u t) \to (P c (TLRef n) (lift (S n) O
u))))))))))) (f3: (\forall (c: C).(\forall (u: T).(\forall (t: T).((ty3 g c u
f1 f2 f3 f4 f5) c0 t2 t3 t4) t5 t6 ((ty3_ind g P f f0 f1 f2 f3 f4 f5) c0 t3
t5 t6))].
-implied let rec tys3_ind (g: G) (c: C) (P: (TList \to (T \to Prop))) (f:
+implied rec lemma tys3_ind (g: G) (c: C) (P: (TList \to (T \to Prop))) (f:
(\forall (u: T).(\forall (u0: T).((ty3 g c u u0) \to (P TNil u))))) (f0:
(\forall (t: T).(\forall (u: T).((ty3 g c t u) \to (\forall (ts:
TList).((tys3 g c ts u) \to ((P ts u) \to (P (TCons t ts) u)))))))) (t:
include "basic_1/wcpr0/defs.ma".
-implied let rec wcpr0_ind (P: (C \to (C \to Prop))) (f: (\forall (c: C).(P c
-c))) (f0: (\forall (c1: C).(\forall (c2: C).((wcpr0 c1 c2) \to ((P c1 c2) \to
-(\forall (u1: T).(\forall (u2: T).((pr0 u1 u2) \to (\forall (k: K).(P (CHead
-c1 k u1) (CHead c2 k u2))))))))))) (c: C) (c0: C) (w: wcpr0 c c0) on w: P c
-c0 \def match w with [(wcpr0_refl c1) \Rightarrow (f c1) | (wcpr0_comp c1 c2
-w0 u1 u2 p k) \Rightarrow (f0 c1 c2 w0 ((wcpr0_ind P f f0) c1 c2 w0) u1 u2 p
-k)].
+implied rec lemma wcpr0_ind (P: (C \to (C \to Prop))) (f: (\forall (c: C).(P
+c c))) (f0: (\forall (c1: C).(\forall (c2: C).((wcpr0 c1 c2) \to ((P c1 c2)
+\to (\forall (u1: T).(\forall (u2: T).((pr0 u1 u2) \to (\forall (k: K).(P
+(CHead c1 k u1) (CHead c2 k u2))))))))))) (c: C) (c0: C) (w: wcpr0 c c0) on
+w: P c c0 \def match w with [(wcpr0_refl c1) \Rightarrow (f c1) | (wcpr0_comp
+c1 c2 w0 u1 u2 p k) \Rightarrow (f0 c1 c2 w0 ((wcpr0_ind P f f0) c1 c2 w0) u1
+u2 p k)].
lemma wcpr0_gen_sort:
\forall (x: C).(\forall (n: nat).((wcpr0 (CSort n) x) \to (eq C x (CSort
include "basic_1/wf3/defs.ma".
-implied let rec wf3_ind (g: G) (P: (C \to (C \to Prop))) (f: (\forall (m:
+implied rec lemma wf3_ind (g: G) (P: (C \to (C \to Prop))) (f: (\forall (m:
nat).(P (CSort m) (CSort m)))) (f0: (\forall (c1: C).(\forall (c2: C).((wf3 g
c1 c2) \to ((P c1 c2) \to (\forall (u: T).(\forall (t: T).((ty3 g c1 u t) \to
(\forall (b: B).(P (CHead c1 (Bind b) u) (CHead c2 (Bind b) u))))))))))) (f1:
include "ground_1/preamble.ma".
-let rec blt (m: nat) (n: nat) on n: bool \def match n with [O \Rightarrow
-false | (S n0) \Rightarrow (match m with [O \Rightarrow true | (S m0)
-\Rightarrow (blt m0 n0)])].
+rec definition blt (m: nat) (n: nat) on n: bool \def match n with [O
+\Rightarrow false | (S n0) \Rightarrow (match m with [O \Rightarrow true | (S
+m0) \Rightarrow (blt m0 n0)])].
| PNil: PList
| PCons: nat \to (nat \to (PList \to PList)).
-let rec PConsTail (hds: PList) on hds: nat \to (nat \to PList) \def \lambda
-(h0: nat).(\lambda (d0: nat).(match hds with [PNil \Rightarrow (PCons h0 d0
-PNil) | (PCons h d hds0) \Rightarrow (PCons h d (PConsTail hds0 h0 d0))])).
+rec definition PConsTail (hds: PList) on hds: nat \to (nat \to PList) \def
+\lambda (h0: nat).(\lambda (d0: nat).(match hds with [PNil \Rightarrow (PCons
+h0 d0 PNil) | (PCons h d hds0) \Rightarrow (PCons h d (PConsTail hds0 h0
+d0))])).
-let rec Ss (hds: PList) on hds: PList \def match hds with [PNil \Rightarrow
-PNil | (PCons h d hds0) \Rightarrow (PCons h (S d) (Ss hds0))].
+rec definition Ss (hds: PList) on hds: PList \def match hds with [PNil
+\Rightarrow PNil | (PCons h d hds0) \Rightarrow (PCons h (S d) (Ss hds0))].
-let rec papp (a: PList) on a: PList \to PList \def \lambda (b: PList).(match
-a with [PNil \Rightarrow b | (PCons h d a0) \Rightarrow (PCons h d (papp a0
-b))]).
+rec definition papp (a: PList) on a: PList \to PList \def \lambda (b:
+PList).(match a with [PNil \Rightarrow b | (PCons h d a0) \Rightarrow (PCons
+h d (papp a0 b))]).
\def
\lambda (n: nat).(match n with [O \Rightarrow O | (S u) \Rightarrow u]).
-let rec plus (n: nat) on n: nat \to nat \def \lambda (m: nat).(match n with
-[O \Rightarrow m | (S p) \Rightarrow (S (plus p m))]).
+rec definition plus (n: nat) on n: nat \to nat \def \lambda (m: nat).(match n
+with [O \Rightarrow m | (S p) \Rightarrow (S (plus p m))]).
-let rec minus (n: nat) on n: nat \to nat \def \lambda (m: nat).(match n with
-[O \Rightarrow O | (S k) \Rightarrow (match m with [O \Rightarrow (S k) | (S
-l) \Rightarrow (minus k l)])]).
+rec definition minus (n: nat) on n: nat \to nat \def \lambda (m: nat).(match
+n with [O \Rightarrow O | (S k) \Rightarrow (match m with [O \Rightarrow (S
+k) | (S l) \Rightarrow (minus k l)])]).
inductive Acc (A: Type[0]) (R: A \to (A \to Prop)): A \to Prop \def
| Acc_intro: \forall (x: A).(((\forall (y: A).((R y x) \to (Acc A R y)))) \to
\lambda (A: Type[0]).(\lambda (x: A).(\lambda (P: ((A \to Prop))).(eq_rect A
x P))).
-implied let rec le_ind (n: nat) (P: (nat \to Prop)) (f: P n) (f0: (\forall
+implied rec lemma le_ind (n: nat) (P: (nat \to Prop)) (f: P n) (f0: (\forall
(m: nat).((le n m) \to ((P m) \to (P (S m)))))) (n0: nat) (l: le n n0) on l:
P n0 \def match l with [le_n \Rightarrow f | (le_S m l0) \Rightarrow (f0 m l0
((le_ind n P f f0) m l0))].
-implied let rec Acc_ind (A: Type[0]) (R: (A \to (A \to Prop))) (P: (A \to
+implied rec lemma Acc_ind (A: Type[0]) (R: (A \to (A \to Prop))) (P: (A \to
Prop)) (f: (\forall (x: A).(((\forall (y: A).((R y x) \to (Acc A R y)))) \to
(((\forall (y: A).((R y x) \to (P y)))) \to (P x))))) (a: A) (a0: Acc A R a)
on a0: P a \def match a0 with [(Acc_intro x a1) \Rightarrow (f x a1 (\lambda
projects / helm.git / commitdiff