Bug fixed: the debrujinate function (hence the one to compute objects height)

[helm.git] / helm / software / components / ng_refiner / esempio.ma

diff --git a/helm/software/components/ng_refiner/esempio.ma b/helm/software/components/ng_refiner/esempio.ma
index d0f6a2e8692f5c64d84ef44779817dfb733af925..8f9604a8524817acdbc1489a7613b43239981310 100644 (file)
--- a/helm/software/components/ng_refiner/esempio.ma
+++ b/helm/software/components/ng_refiner/esempio.ma
@@ -17,6 +17,13 @@ include "nat/plus.ma".
 definition hole : ∀A:Type.A → A ≝ λA.λx.x.
 definition id : ∀A:Type.A → A ≝ λA.λx.x.
 
+(* Common case in dama, reduction with metas
+inductive list : Type := nil : list | cons : nat -> list -> list.
+let rec len l := match l with [ nil => O | cons _ l => S (len l) ].
+axiom lt : nat -> nat -> Prop.
+axiom foo : ∀x. Not (lt (hole ? x) (hole ? O)) = (lt x (len nil) -> False).
+*) 
+
 (* meta1 Vs meta2 with different contexts
 axiom foo: 
   ∀P:Type.∀f:P→P→Prop.∀x:P.
@@ -49,7 +56,7 @@ axiom foo:
 *)  
    
 alias num (instance 0) = "natural number".
-axiom foo: (12+12) = (12+11).
+axiom foo: (100+111) = (100+110). 
 
 
     (id ?(id ?(id ?(id ? (100+100))))) =