Skip to content

Commit

Permalink
Intuitionize CCfld from cncrng to cnfldexp (#4683)
Browse files Browse the repository at this point in the history
* Rename addid2 to addlid in iset.mm

This matches rename already done in set.mm.

* Rename mulid2 to mullid in iset.mm

Matches rename already done in set.mm.

* Rename mulrid to mulridx in iset.mm

Already renamed in set.mm.

* Rename mulid1 to mulrid in iset.mm

Already renamed in set.mm.

* copy cncrng from set.mm to iset.mm

* copy cnring from set.mm to iset.mm

* copy cnfld0 and cnfld1 from set.mm to iset.mm

* copy cnfldneg from set.mm to iset.mm

* Add cnfldplusf to iset.mm

Stated as in set.mm.  The proof needs a little bit of intuitionizing but
is basically the set.mm proof.

* Add cnfldsub to iset.mm

Stated as in set.mm.  The proof needs a little bit of intuitionizing but
is basically the set.mm proof.

* add cndrng to mmil.html

* Add cnflddiv to mmil.html

* add cnfldinv to mmil.html

* Add cnfldmulg to iset.mm

Copied from set.mm without change.

* Add cnfldexp to iset.mm

Stated as in set.mm.  The proof needs a little intuitionizing but is
basically the set.mm proof.

* add cnsrng to mmil.html
  • Loading branch information
jkingdon authored Mar 1, 2025
1 parent a5c3929 commit 5375a34
Show file tree
Hide file tree
Showing 3 changed files with 183 additions and 56 deletions.
3 changes: 2 additions & 1 deletion iset-discouraged
Original file line number Diff line number Diff line change
Expand Up @@ -63,6 +63,7 @@
"ax-addcom" is used by "addcom".
"ax-addf" is used by "addcncntop".
"ax-addf" is used by "addex".
"ax-addf" is used by "cnfldplusf".
"ax-addrcl" is used by "readdcl".
"ax-arch" is used by "arch".
"ax-caucvg" is used by "caucvgre".
Expand Down Expand Up @@ -327,7 +328,7 @@ New usage of "ax-1re" is discouraged (1 uses).
New usage of "ax-addass" is discouraged (1 uses).
New usage of "ax-addcl" is discouraged (1 uses).
New usage of "ax-addcom" is discouraged (1 uses).
New usage of "ax-addf" is discouraged (2 uses).
New usage of "ax-addf" is discouraged (3 uses).
New usage of "ax-addrcl" is discouraged (1 uses).
New usage of "ax-arch" is discouraged (1 uses).
New usage of "ax-caucvg" is discouraged (1 uses).
Expand Down
Loading

0 comments on commit 5375a34

Please sign in to comment.