All weakly positive types but imbricated ones are now accepted

[helm.git] / helm / software / matita / tests / ng_elim.ma

diff --git a/helm/software/matita/tests/ng_elim.ma b/helm/software/matita/tests/ng_elim.ma
index c3b3d09bca282ee37756171bbe539602924ce191..3ef667bdb2a53c62eb79b1bc95f31d0867fc596b 100644 (file)
--- a/helm/software/matita/tests/ng_elim.ma
+++ b/helm/software/matita/tests/ng_elim.ma
@@ -26,6 +26,17 @@ nlet rec nat_rec (Q: nat → Type) H_O H_S x_1 on x_1 : Q x_1 ≝
   | S x_2 ⇒ H_S x_2 (nat_rec Q H_O H_S x_2)
   ].
 
+
+ninductive ord: Type ≝
+   OO: ord
+ | OS: ord → ord
+ | OLim: (nat → ord) → ord.
+
+nlet rec ord_rect (Q_: (∀ (x_3: (ord)).Type)) H_OO H_OS H_OLim x_3 on x_3: (Q_ x_3) ≝
+ (match x_3 with [OO ⇒ (H_OO) | (OS x_4) ⇒ (H_OS x_4 (ord_rect Q_ H_OO H_OS H_OLim (x_4))) | (OLim x_6) ⇒ (H_OLim x_6 (λx_5.(ord_rect Q_ H_OO H_OS H_OLim (x_6 x_5))))]).
+
+
+
 naxiom P: nat → Prop.
 naxiom p: ∀m. P m.