From 22b65a1bf3758393894d43373bf14ca73d334b02 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Jun 2005 10:50:31 +0000 Subject: [PATCH] Harder test (with empty inductive types and left and right arguments to inductive types). It does not compile yet. --- helm/matita/tests/match_inference.ma | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/helm/matita/tests/match_inference.ma b/helm/matita/tests/match_inference.ma index a84b3c373..1e43ce145 100644 --- a/helm/matita/tests/match_inference.ma +++ b/helm/matita/tests/match_inference.ma @@ -6,12 +6,24 @@ inductive nat:Set \def | O : nat | S : nat \to nat. -inductive empty : Set \def . - definition pos2nat : pos \to nat \def \lambda x:pos . match x with [ one \Rightarrow O | (next z) \Rightarrow O]. -definition empty2nat : empty \to nat \def - \lambda x : empty . S (match x in empty with []). \ No newline at end of file +inductive empty (x:nat) : nat \to Set \def . + +definition empty2nat : (empty O O) \to nat \def + \lambda x : (empty O O). S (match x in empty with []). + +inductive le (n:nat) : nat \to Prop \def + | le_n : le n n + | le_S : \forall m:nat. le n m \to le n (S m). + +inductive True : Prop \def + I : True. + +definition r : True \def + match (le_n O) with + [ le_n \Rightarrow I + | (le_S y p') \Rightarrow I ]. -- 2.39.2