diff options
| author | filliatr | 2001-04-11 12:41:41 +0000 |
|---|---|---|
| committer | filliatr | 2001-04-11 12:41:41 +0000 |
| commit | 4ac0580306ea9e45da1863316936d700969465ad (patch) | |
| tree | bf7595cd76895f3a349e7e75ca9d64231b01dcf8 /theories/IntMap | |
| parent | 8a7452976731275212f0c464385b380e2d590f5e (diff) | |
documentation automatique de la bibliothèque standard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1578 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/IntMap')
| -rw-r--r-- | theories/IntMap/Adalloc.v | 3 | ||||
| -rw-r--r-- | theories/IntMap/Adist.v | 4 | ||||
| -rw-r--r-- | theories/IntMap/Map.v | 4 | ||||
| -rw-r--r-- | theories/IntMap/intro.tex | 5 |
4 files changed, 11 insertions, 5 deletions
diff --git a/theories/IntMap/Adalloc.v b/theories/IntMap/Adalloc.v index 58d02676e5..47cff4f8e9 100644 --- a/theories/IntMap/Adalloc.v +++ b/theories/IntMap/Adalloc.v @@ -209,7 +209,8 @@ Section AdAlloc. Unfold in_dom. Intro. Rewrite (ad_alloc_opt_allocates_1 m). Reflexivity. Qed. - (* Moreover, this is optimal: all addresses below (ad_alloc_opt m) are in dom m: *) + (* Moreover, this is optimal: all addresses below [(ad_alloc_opt m)] + are in [dom m]: *) Lemma convert_xH : (convert xH)=(1). Proof. diff --git a/theories/IntMap/Adist.v b/theories/IntMap/Adist.v index b9cee92ef1..ec08fb35f1 100644 --- a/theories/IntMap/Adist.v +++ b/theories/IntMap/Adist.v @@ -258,10 +258,10 @@ Qed. (*s $d$ is an ultrametric distance, that is, not only $d(a,a')\leq d(a,a'')+d(a'',a')$, but in fact $d(a,a')\leq max(d(a,a''),d(a'',a'))$. This means that $min(pd(a,a''),pd(a'',a'))<=pd(a,a')$ (lemma [ad_pdist_ultra] below). - This follows from the fact that $a \Ra |a| = 1/2^\TT{ad\_plength}(a))$ + This follows from the fact that $a \Ra |a| = 1/2^\texttt{ad\_plength}(a))$ is an ultrametric norm, i.e. that $|a-a'| \leq max (|a-a''|, |a''-a'|)$, or equivalently that $|a+b|<=max(|a|,|b|)$, i.e. that - min $(\TT{ad\_plength}(a), \TT{ad\_plength}(b)) \leq \TT{ad\_plength} (a~\TT{xor}~ b)$ + min $(\texttt{ad\_plength}(a), \texttt{ad\_plength}(b)) \leq \texttt{ad\_plength} (a~\texttt{xor}~ b)$ (lemma [ad_plength_ultra]). *) diff --git a/theories/IntMap/Map.v b/theories/IntMap/Map.v index 2f1c47bb69..ca436cddb5 100644 --- a/theories/IntMap/Map.v +++ b/theories/IntMap/Map.v @@ -181,7 +181,7 @@ Section MapDefs. Intros. Case b; Trivial. Qed. - (* + (*i Lemma MapGet_M2_bit_0_1' : (m,m',m'',m''':Map) (a:ad) (MapGet (if (ad_bit_0 a) then (M2 m m') else (M2 m'' m''')) a)= (MapGet (if (ad_bit_0 a) then m' else m'') (ad_div_2 a)). @@ -192,7 +192,7 @@ Section MapDefs. Intros. Rewrite H0. Apply MapGet_M2_bit_0_1. Assumption. Case (ad_bit_0 a); Auto. Qed. - *) + i*) Lemma MapGet_if_same : (m:Map) (b:bool) (a:ad) (MapGet (if b then m else m) a)=(MapGet m a). Proof. diff --git a/theories/IntMap/intro.tex b/theories/IntMap/intro.tex new file mode 100644 index 0000000000..cfaae2468b --- /dev/null +++ b/theories/IntMap/intro.tex @@ -0,0 +1,5 @@ +\section{IntMap}\label{IntMap} + +This library contains a data structure for finite sets implemented by +an efficient structure of map (trees indexed by binary integers). + |