X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Ftests%2Fng_elim.ma;h=b67401fde0a32273ccabdcdf6e3b19c1ab1f2834;hb=c78edd42f3ebc7c82bb319b876908bf17288ab04;hp=3ef667bdb2a53c62eb79b1bc95f31d0867fc596b;hpb=4e98c439731c6e110430a6c5217274215bf403b6;p=helm.git diff --git a/helm/software/matita/tests/ng_elim.ma b/helm/software/matita/tests/ng_elim.ma index 3ef667bdb..b67401fde 100644 --- a/helm/software/matita/tests/ng_elim.ma +++ b/helm/software/matita/tests/ng_elim.ma @@ -48,8 +48,7 @@ nlet rec le_rect n N (Q_: (∀ m.(∀ x_4.(∀ (x_3: (le n N m x_4)).Type)))) H_ on x_3: (Q_ m x_4 x_3) ≝ (match x_3 with [len ⇒ (H_len) | (leS m q x_5) ⇒ (H_leS m q x_5 (le_rect n N Q_ H_len H_leS ? ? x_5))]). - - +(* nlet rec le_rec' (n:nat) (Q: ∀D1:nat.∀D2: P D1. le n D1 D2 → Type) (p1: ?) (p2: ?) (D1:nat) (D2:P D1) (x: le n D1 D2) on x : Q D1 D2 x ≝ match x with [ len ⇒ p1 @@ -63,4 +62,13 @@ nlet rec le_rec (n:nat) (Q: ∀D1:nat.∀D2: P D1. le n D1 D2 → Type) (p1: ?) ##] ## |##*: ## skip; ## ] -nqed. \ No newline at end of file +nqed.*) + +include "list/list.ma". + +ninductive ii: Type ≝ + kk: list ii → ii. + +nlet rec ii_rect (Q_: (∀(x_16: ii).Type)) H_kknil H_kkcons x_16 on x_16: (Q_ x_16) ≝ + (match x_16 with + [ kk x_17 ⇒ list_rect ii (λx_17.Q_ (kk x_17)) H_kknil (λw.H_kkcons w (ii_rect Q_ H_kknil H_kkcons w)) x_17 ]). \ No newline at end of file