diff options
author | Stephane Glondu <steph@glondu.net> | 2012-08-20 18:27:01 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-08-20 18:27:01 +0200 |
commit | e0d682ec25282a348d35c5b169abafec48555690 (patch) | |
tree | 1a46f0142a85df553388c932110793881f3af52f /test-suite/success/RecTutorial.v | |
parent | 86535d84cc3cffeee1dcd8545343f234e7285530 (diff) |
Imported Upstream version 8.4dfsgupstream/8.4dfsg
Diffstat (limited to 'test-suite/success/RecTutorial.v')
-rw-r--r-- | test-suite/success/RecTutorial.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index 64048fe2..459645f6 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -378,18 +378,18 @@ Inductive itree : Set := Definition isingle l := inode l (fun i => ileaf). -Definition t1 := inode 0 (fun n => isingle (Z_of_nat (2*n))). +Definition t1 := inode 0 (fun n => isingle (Z.of_nat (2*n))). Definition t2 := inode 0 (fun n : nat => - inode (Z_of_nat n) - (fun p => isingle (Z_of_nat (n*p)))). + inode (Z.of_nat n) + (fun p => isingle (Z.of_nat (n*p)))). Inductive itree_le : itree-> itree -> Prop := | le_leaf : forall t, itree_le ileaf t | le_node : forall l l' s s', - Zle l l' -> + Z.le l l' -> (forall i, exists j:nat, itree_le (s i) (s' j)) -> itree_le (inode l s) (inode l' s'). @@ -424,7 +424,7 @@ Qed. Inductive itree_le' : itree-> itree -> Prop := | le_leaf' : forall t, itree_le' ileaf t | le_node' : forall l l' s s' g, - Zle l l' -> + Z.le l l' -> (forall i, itree_le' (s i) (s' (g i))) -> itree_le' (inode l s) (inode l' s'). |