• Robbert Krebbers's avatar
    Disambiguate Haskell-style notations for partially operators. · 45690e49
    Robbert Krebbers authored
    For example, change `(!! i)` into `(.!! x)` so that `!!` can also be used as
    a prefix, as done in VST for example.
    
    This closes issue #42.
    
    I have used the `sed` script below. This script took care of nearly all uses
    apart from a few occurrences where a space was missing, e.g. `(,foo)`. In
    this case, `coqc` will just fail, allowing one to patch up things manually.
    
    The script is slightly too eager on Iris developments, where it also replaces
    `($ ...)` introduction patterns. When porting Iris developments you thus may
    want to remove the line for `$`.
    
    ```
    sed '
    s/(= /(.= /g;
    s/ =)/ =.)/g;
    s/(≠ /(.≠ /g;
    s/ ≠)/ ≠.)/g;
    s/(≡ /(.≡ /g;
    s/ ≡)/ ≡.)/g;
    s/(≢ /(.≢ /g;
    s/ ≢)/ ≢.)/g;
    s/(∧ /(.∧ /g;
    s/ ∧)/ ∧.)/g;
    s/(∨ /(.∨ /g;
    s/ ∨)/ ∨.)/g;
    s/( /(. /g;
    s/ )/ .)/g;
    s/(→ /(.→ /g;
    s/ →)/ →.)/g;
    s/($ /(.$ /g;
    s/(∘ /(.∘ /g;
    s/ ∘)/ ∘.)/g;
    s/(, /(., /g;
    s/ ,)/ ,.)/g;
    s/(∘ /(.∘ /g;
    s/ ∘)/ ∘.)/g;
    s/(∪ /(.∪ /g;
    s/ ∪)/ ∪.)/g;
    s/(⊎ /(.⊎ /g;
    s/ ⊎)/ ⊎.)/g;
    s/(∩ /(.∩ /g;
    s/ ∩)/ ∩.)/g;
    s/(∖ /(.∖ /g;
    s/ ∖)/ ∖.)/g;
    s/(⊆ /(.⊆ /g;
    s/ ⊆)/ ⊆.)/g;
    s/(⊈ /(.⊈ /g;
    s/ ⊈)/ ⊈.)/g;
    s/(⊂ /(.⊂ /g;
    s/ ⊂)/ ⊂.)/g;
    s/(⊄ /(.⊄ /g;
    s/ ⊄)/ ⊄.)/g;
    s/(∈ /(.∈ /g;
    s/ ∈)/ ∈.)/g;
    s/(∉ /(.∉ /g;
    s/ ∉)/ ∉.)/g;
    s/(≫= /(.≫= /g;
    s/ ≫=)/ ≫=.)/g;
    s/(!! /(.!! /g;
    s/ !!)/ !!.)/g;
    s/(⊑ /(.⊑ /g;
    s/ ⊑)/ ⊑.)/g;
    s/(⊓ /(.⊓ /g;
    s/ ⊓)/ ⊓.)/g;
    s/(⊔ /(.⊔ /g;
    s/ ⊔)/ ⊔.)/g;
    s/(:: /(.:: /g;
    s/ ::)/ ::.)/g;
    s/(++ /(.++ /g;
    s/ ++)/ ++.)/g;
    s/(≡ₚ /(.≡ₚ /g;
    s/ ≡ₚ)/ ≡ₚ.)/g;
    s/(≢ₚ /(.≢ₚ /g;
    s/ ≢ₚ)/ ≢ₚ.)/g;
    s/(::: /(.::: /g;
    s/ :::)/ :::.)/g;
    s/(+++ /(.+++ /g;
    s/ +++)/ +++.)/g;
    ' -i $(find -name "*.v")
    ```
    45690e49
Name
Last commit
Last update
..
base.v Loading commit data...
binders.v Loading commit data...
boolset.v Loading commit data...
coPset.v Loading commit data...
countable.v Loading commit data...
decidable.v Loading commit data...
fin.v Loading commit data...
fin_map_dom.v Loading commit data...
fin_maps.v Loading commit data...
fin_sets.v Loading commit data...
finite.v Loading commit data...
functions.v Loading commit data...
gmap.v Loading commit data...
gmultiset.v Loading commit data...
hashset.v Loading commit data...
hlist.v Loading commit data...
infinite.v Loading commit data...
lexico.v Loading commit data...
list.v Loading commit data...
listset.v Loading commit data...
listset_nodup.v Loading commit data...
mapset.v Loading commit data...
namespaces.v Loading commit data...
nat_cancel.v Loading commit data...
natmap.v Loading commit data...
nmap.v Loading commit data...
numbers.v Loading commit data...
option.v Loading commit data...
orders.v Loading commit data...
pmap.v Loading commit data...
prelude.v Loading commit data...
pretty.v Loading commit data...
proof_irrel.v Loading commit data...
propset.v Loading commit data...
relations.v Loading commit data...
sets.v Loading commit data...
sorting.v Loading commit data...
streams.v Loading commit data...
stringmap.v Loading commit data...
strings.v Loading commit data...
tactics.v Loading commit data...
telescopes.v Loading commit data...
vector.v Loading commit data...
zmap.v Loading commit data...