Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Avoid relying on Add Field calling Add Ring. #81

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Avoid relying on Add Field calling Add Ring. #81

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions orders/rationals.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@ Section rationals_and_another_rationals.
Context `{Rationals Q2} `{Apart Q2} `{!TrivialApart Q2} `{!FullPseudoSemiRingOrder (A:=Q2) Q2le Q2lt}
{f : Q1 → Q2} `{!SemiRing_Morphism f}.

Add Ring Q1 : (F_R (stdlib_field_theory Q1)).
Add Field Q1 : (stdlib_field_theory Q1).

Notation i_to_r := (integers.integers_to_ring (SRpair nat) Q1).
Expand Down Expand Up @@ -93,6 +94,7 @@ Instance rationals_lt `{Rationals Q} : Lt Q | 10 := dec_lt.
Section default_order.
Context `{Rationals Q} `{Apart Q} `{!TrivialApart Q}.

Add Ring R: (F_R (stdlib_field_theory Q)).
Add Field F: (stdlib_field_theory Q).
Notation n_to_sr := (naturals_to_semiring nat Q).

Expand Down
1 change: 1 addition & 0 deletions theory/dec_fields.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -205,6 +205,7 @@ Section from_stdlib_field_theory.
`{!Proper (Fe ==> Fe) Fnegate}
`{!Proper (Fe ==> Fe) Frecip}.

Add Ring F2 : (F_R ftheory).
Add Field F2 : ftheory.

Definition from_stdlib_field_theory: @DecField F Fe Fplus Fmult Fzero Fone Fnegate Frecip.
Expand Down
1 change: 1 addition & 0 deletions theory/int_pow.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ Require Import
Section int_pow_properties.
Context `{DecField A} `{∀ x y, Decision (x = y)} `{Integers B} `{!IntPowSpec A B ipw}.

Add Ring A : (F_R (dec_fields.stdlib_field_theory A)).
Add Field A : (dec_fields.stdlib_field_theory A).
Add Ring B : (rings.stdlib_ring_theory B).

Expand Down