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

Jump to bottom

prob interface #51

Open
affeldt-aist opened this issue Feb 27, 2021 · 2 comments
Open

prob interface #51

affeldt-aist opened this issue Feb 27, 2021 · 2 comments

Comments

@affeldt-aist
Copy link
Owner

infotheo/lib/Reals_ext.v

Line 387 in fdba7c4

Definition mk_ (q : R) (Oq1 : 0 <= q <= 1) := mk (introT (@leR2P _ _ _) Oq1).

Since we're favoring a structure with an inequality in bool for prob, the constructor mk_ might turn out to be superfluous after all. Investigate its removal.

Cc: @t6s
@t6s
Copy link
Collaborator

t6s commented Feb 27, 2021 •
edited by affeldt-aist
Loading

How about renaming closed to lt2W?

NB(rei): has been taken care of by PR #52

@t6s
Copy link
Collaborator

t6s commented Feb 27, 2021 •
edited by affeldt-aist
Loading

Oops this comment was not meant for this issue.

@affeldt-aist affeldt-aist modified the milestones: 0.3.2, 0.3.3 Mar 19, 2021
@affeldt-aist affeldt-aist modified the milestones: 0.3.3, 0.3.4 Jun 7, 2021
@affeldt-aist affeldt-aist modified the milestones: 0.3.4, 0.3.5 Nov 20, 2021
@affeldt-aist affeldt-aist modified the milestones: 0.3.5, 0.3.6 Jan 3, 2022
@affeldt-aist affeldt-aist modified the milestones: 0.3.6, 0.3.7 Feb 14, 2022
@affeldt-aist affeldt-aist modified the milestones: 0.3.7, 0.3.8 Apr 14, 2022
@affeldt-aist affeldt-aist removed this from the 0.3.8 milestone Nov 1, 2022
@affeldt-aist affeldt-aist added this to the 0.6.0 milestone Nov 20, 2023
@affeldt-aist affeldt-aist modified the milestones: 0.6.0, 0.6.1 Dec 1, 2023
@affeldt-aist affeldt-aist removed this from the 0.6.1 milestone Jun 14, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@t6s @affeldt-aist