From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 12 May 2009 22:16:00 +0000 (+0000)
Subject: Do we really want to generate eliminators for nested data types? :-)
X-Git-Tag: make_still_working~3986
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=45cf52fb31fdefdb17377aa14902d2a1ff1b11d2;p=helm.git

Do we really want to generate eliminators for nested data types? :-)
---

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