Stdlib2: get started #14

vbgl · 2019-02-18T13:04:03Z

Because at some point, we should get started.

Zimmi48 · 2019-02-18T13:39:37Z

Please update the README as part of this PR to say whether code contributions are welcome or still not expected at this stage. You don't want to give the wrong impression to people. Ideally, write up about the current state in more details so that (even if code contributions are not expected), people are not left figuring the plan by themselves if they want to keep commenting in the issue tracker. Or if even commenting on the issue tracker should be restricted to a few topics for now because it is too early for some others, please say so.

gmalecha · 2019-02-18T18:59:55Z

src/prelude.v

+Global Unset Printing Implicit Defensive.
+Global Set Primitive Projections.
+
+(** Plugins loaded initially *)


What is the impact of this? Is it still the case that plugin loading is recursive? Does this mean that any file that uses stdlib2 must load ltac, ssrmatching, and ssreflect? If that is the case, I personally find this sub-optimal (supposing it is possible to get around this).

If by loading you mean dynamically linked, then the answer is yes, I believe. What are your concerns?

Two things came to mind which made me think about it, maybe they don't make much difference.

The cost of loading them (which is probably fast and small so maybe not a big deal?).

The fact that this makes versioning them impossible. If a new release of Ltac is released, then you have to rebuild the entire universe. This might be unavoidable, so maybe not putting it here doesn't change much.

gmalecha · 2019-02-18T19:04:16Z

src/bool.v

+
+(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **)
+
+Require Import functions.


I will preface this by saying that I don't use ssreflect, but it seems odd that most basic data types live in the file datatypes.v which is 131 lines long. Then there is the bool datatype that lives in bool.v which is 2029 lines long. Would anyone object to splitting this file and putting the actual bool type in either its own small file or in the datatypes.v file and then renaming this file into deciable_predicates.v or something like that.

I guess that's a pragmatic choice because bool comes with a much richer theory than unit or option. Can you make explicit your concrete concern?

Perhaps this is more a comment than a concern. To me, the contents of this file contains two things:

the bool data type.

a particular way that some people (maybe most? maybe most should?) use the bool datatype.
Is it desireable to put both in the same file? One might argue that option has a "rich theory", e.g. it is a functor, an applicative, a monad, traversable. That's pretty cool, should all of those go in datatypes.v?

One argument for yes would be: loading files from disk is expensive and "all Coq programmers use (or should use) these definitions so so they'll appreciate the definitions". I could buy that, though it always makes me a big scared. A Haskell programmer might say "I can't imagine programming without the category of Xxxx, so let's put that in the prelude". :-)

Another thought would be, a new person comes to Coq and says, "this seems pretty cool. I know a lot about booleans, maybe I'll take a look at bool.v to see what Coq has" and then says "wow, Coq is complicated."

Another thought (perhaps more pragmatic?) would be: what do you get if you run SearchAbout bool.?

gmalecha · 2019-02-18T19:07:27Z

src/datatypes.v

+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+Require Import prelude ssreflect prop equality.


What is the motivation for having all of the core datatype in the same file? Some of the initial issues on this repository suggested that we have a set of core definitions that go along with different types, e.g. a relation #4. If we go that route, does it make sense to make separate modules for each data type and then export them each datatypes.v?

I guess we can still reorganize when adding new theory or types coming with these datatypes, splitting if the file becomes too big.

Perhaps the idea is that nothing here is set in stone, which is perfectly fine, even expected at this point. I was wondering if there is some discipline which is codified informally in this PR that is meant to be suggestive of how stdlib2 should be developed.

gmalecha · 2019-02-18T19:09:58Z

src/datatypes.v

+Notation odflt := Option.default.
+Notation obind := Option.bind.
+Notation omap := Option.map.
+Notation some := (@Some _) (only parsing).


Is it really ideal to put make these global notations in the prelude? Am I wrong, or is this practically this is like making them keywords in Coq? e.g. they can't be used as variable names, etc.

Good question. I'm never sure of how implicit keyword declarations work with notations, we'd have to check this.

No, they are not keywords:

Notation x := 3. Lemma foo : forall x, x = 3. Proof intros. Fail reflexivity. Abort.

Interesting. How does the system know when to resolve them as one or the other?

https://coq.inria.fr/distrib/current/refman/user-extensions/syntax-extensions.html#abbreviations
So Notation foo := bla. doesn't make foo a keyword, Notation "'foo'" := bla. does make foo a keyword.

gmalecha · 2019-02-18T19:12:29Z

src/datatypes.v

+
+(** [option A] is the extension of [A] with an extra element [None] *)
+
+Variant option (A : Type) : Type :=


Will the core datatypes still not be universe polymorphic? My understanding (perhaps I am wrong) is that template universe polymorphism is (or could be) on the chopping block for future versions on Coq.

Ideally, we shouldn't rely on template polymorphism indeed. On the other hand, universe polymorphism as of today does not subsume template polymorphism. Maybe we should open an issue to get the opinion of universe experts.

If I understand correctly, all inductive definitions should ideally be made polymorphic and cumulative but there's something to do to make sure that this allows instantiating with Prop still.

Is auto template on in stdlib2?
For option full polymorphism should subsume template (option can't be Prop).

gmalecha · 2019-02-18T19:14:40Z

src/datatypes.v

+
+(** [sum A B], also noted [A + B] is the disjoint sum of datatypes [A] and [B]. *)
+Variant sum A B : Type :=
+| Left of A


I've never seen this notation before and it seems inconsistent with the rest of the file.

Right, we should probably use it from the start. Note that I believe it is being merge to gallina proper.

Note that I believe it is being merge to gallina proper.

There is no opened PR doing this but I definitely support the idea of merging this into proper Gallina (ideally with refined syntax where you can't use & before of).

Personally, I don't like this syntax and I believe that it complicates things for a special-case. It isn't much shorter than:

Variant sum A B : Type := | Left (_ : A) | Right (_ : B).

It is slightly longer, but:

more consistent

provides a place to document names

provides a place to make things implicit

makes it easy to change the type with minimal typographic changes (e.g. making it indexed)

adds a new keyword "of" to the language.

Personally, I don't like this syntax

It's not meant to be mandatory, of course. I personally like it.

gmalecha · 2019-02-18T19:16:39Z

src/nat.v

+
+Arguments S _%nat_scope.
+
+Notation "0" := O : nat_scope.


Don't we have numeral parsing now? Does it not work well enough?

Oh, this was not in my branch. @vbgl do you remember why you added it? Maybe it was before numeral notations were merged.

gmalecha · 2019-02-18T19:19:00Z

src/bool.v

+(**  Allow the direct application of a reflection lemma to a boolean assertion.  **)
+Coercion elimT : reflect >-> Funclass.
+
+#[universes(template)]


Repeating an earlier comment, are templated universes going to stick around long term?

My guess is that this annotation was added because of a misleading warning emitted by master at some point. It should be removed.

SkySkimmer · 2019-02-18T20:33:36Z

src/bool.v

+Coercion elimT : reflect >-> Funclass.
+
+#[universes(template)]
+Variant implies P Q := Implies of P -> Q.


This one can be Prop, so unless nobody uses that feature it has to be template for now.

herbelin · 2019-02-19T09:29:45Z

@vbgl: Thanks a lot for starting as we indeed need concrete matter for discussions to happen. Here are first quick comments to start with:

I believe that a discussion on a lowercase/uppercase policy for filename should happen. The standard library has currently capitalized file names which suggests that the transition could be better with capitalized file names.
If there is a consensus to adopt ssr features of universal purpose in the stdlib2 (and we may think there will be some, e.g. for pattern selection), I don't think it needs the ssr prefix. It shall simply be a "universal" Coq concept.
I don't know well lock and other "<hidden n >" things, but my feeling was these were hacks. Can someone justify that it is worth to be in a library rather than provided at the level of the implementation of Coq?

maximedenes · 2019-02-19T09:43:16Z

Thanks for the feedback, @herbelin

the transition could be better with capitalized file names

I'm not aware of any technical reasons why one or the other would be better. Is there any? I personally don't mind either way.

I don't think it needs the ssr prefixI guess

IIUC, you mean that ssrmatching could be renamed into matching. I tend to agree with that. In fact, I did it for other (.v) files. For this one, I was probably fearing that it could collide with an already existing matching.ml file in Coq, but is seems that there's none.

I don't know well lock and other "<hidden n >" things, but my feeling was these were hacks. Can someone justify that it is worth to be in a library rather than provided at the level of the implementation of Coq?

I wouldn't say lock is so much of hack, it exposes an equation and hides the computational behavior in a way that is fairly idiomatic in the language (it simply makes it generic). Still, it would probably be nice to provide a more robust implementation of these indeed, but I'm not sure how it could be done. I see it as temporary measures until something better is implemented.

Generally speaking, we are happy to try to improve the implementation of Coq rather than circumventing problems in the library (that's what we are doing for the issues we face with primitive projections, for example). But due to limited manpower, we sometimes have to settle for temporary solutions.

gares · 2019-02-19T12:12:39Z

src/abstract.v

+(* To focus non-ssreflect tactics on a subterm, eg vm_compute. *)
+(* Usage:                                                      *)
+(*   elim/abstract_context: (pattern) => G defG.               *)
+(*   vm_compute; rewrite {}defG {G}.                           *)


I've recently discovered that rewrite {G}defG would work here (the same behavior was made consistent in other tactics very recently) so you should update the comment.

gares · 2019-02-19T12:29:56Z

src/nat.v

+
+Inductive nat :=
+| O
+| S `(nat).


I think this use of backtick is not documented (and not strictly needed either).

gares · 2019-02-19T12:31:06Z

src/prop.v

+   | match goal with H : ~ _ |- _ => solve [case H; trivial] end ].
+
+(* Quicker done tactic not including split, syntax: /0/ *)
+Ltac ssrdone0 :=


I've seen these two tactics also in bool

gmalecha · 2019-02-19T12:31:28Z

I'm on the fence about capital vs lower case names for different things: modules, types, constructors, names, tactics. I do think consistency across the library is important though. We should also note whether capital means CamelCase, or if lower case means snake_case. All lower case with no way to separate works can sometimes be difficult to follow.

src/ssreflect.v

gares · 2019-02-19T12:33:14Z

src/ssreflect.v

+
+(**  Constants for tactic-views  **)
+#[universes(template)]
+Inductive external_view : Type := tactic_view of Type.


This should be remove, it is not used (maybe it should also be remove from master if it happens to be there)

gares · 2019-02-19T12:33:33Z

src/ssreflect.v

+   ].
+
+(* Quicker done tactic not including split, syntax: /0/ *)
+Ltac ssrdone0 :=


hem, yet another copy

gares · 2019-02-19T12:36:15Z

<hidden n > is infrastructure for the abstract: tactic, it is not a hack.

gares · 2019-02-19T12:46:07Z

Looks like a good start to me. I've only question because I don't see what is the plan. The "bios" of ssr was split, eg abstract.v or congr.v, but the code is monolitic. So if you load ssreflect_plugin.cmxs you now need to load more .v files in order to have it actually working, and prelude.v does not load any of the bios but loads the plugin. So I'm a bit lost.

herbelin · 2019-02-19T18:41:59Z

<hidden n > is infrastructure for the abstract: tactic, it is not a hack.

I called it hack in the sense that I don't see why the infrastructure for abstract: should show through in the notation system. This does not look as the right separation of concerns.

When I see a notation like "T (* n *)", I also remain skeptical about whether this is something we really want to show as an example of "good code".

herbelin · 2019-02-19T19:05:24Z

I'm not aware of any technical reasons why one or the other would be better. Is there any? I personally don't mind either way.

There is no technical reasons (a priori) why one or the other would be better, but we have to think to the implications.

For instance, I guess we want to have the style of module names to be the same as the style of file names. So, moving to lowercase would mean moving module names to lowercase too.

There is also an implicit usage that we follow conventions consistent with OCaml and OCaml has uppercase for modules (even if for some reason which I forgot, or maybe there is no real reason, the file names are conventionally obtained by lowering the first letter of the module name).

More generally, settling a number of conventions or homogeneity of style such as using CamlCase or snake_case (referring to @gmalecha's comment), or some other conventions for propositions, lemma names, constructors, may help the users of the library to identify what is what and to give a feeling of unity. For instance, the Classes library has the convention to have the class with a capital and the constructors and instances lowercase, but other libraries have other conventions. The choice of case is actually not the only thing to exploit. We can exploit prefixes such as is_, or pred_, or fun_.

I think that if one of you (@maximedenes, @vbgl) could make a summary of the existing conventions around, that would be very helpful.

Zimmi48 · 2019-02-19T19:22:07Z

Definitely agree that setting conventions is going to help contributors and keep the whole thing clean. Not everything has to be decided just now (obviously) but starting a document about the conventions (even if just a stub, even if some conventions are not set in stone and some are just documented as not yet decided) would be a huge win and the sooner the better 🤗

herbelin · 2019-02-19T19:40:50Z

More comments:

Like @gares, I'm a bit lost with the plan. At the current stage, this looks more like a copy-paste of ssreflect or mathcomp files than a consensual proposal synthetizing propositions from a community of experienced users. We are several people with a lot to say about how to develop a standard library. Where is the plan to make a synthesis of the good ideas present here and there? Where is the plan to capitalize on our experience to avoid known pitfalls?

A better way to proceed might be to take excerpts of existing proposals, e.g. an excerpt from the current stdlib, an excerpt from stdpp, an excerpt from mathcomp, an excerpt from HoTT, etc. and that we comment them as if we were commenting a PR, progressively building a document of conventions, of definitions, theorems, techniques we want to see present. We could typically start such comparison with the logic (ex, sig, ...), with the boolean (and boolean reflection), with the lists, ...

andres-erbsen · 2019-02-19T19:44:22Z

Can we please have no canonical structures in stdlib2? I can think of perhaps 5 people who might understand how to debug or build stuff on top of these.

More generally: This bulk import, if merged, would set a direction for the rest of the project. Or perhaps it looks like a direction has already been set. I agree that ssreflect is one major lineage of Coq development to consider, but at the very least we should reach overwhelming agreement on what exactly is gained or traded away by mimicking that design. For example, I would love to have an actual discussion about modularity mechanisms, as I tried to start in #13.

Zimmi48 · 2019-02-19T20:02:57Z

At the current stage, this looks more like a copy-paste of ssreflect or mathcomp files than a consensual proposal synthetizing propositions from a community of experienced users.

A better way to proceed might be to take excerpts of existing proposals, e.g. an excerpt from the current stdlib, an excerpt from stdpp, an excerpt from mathcomp, an excerpt from HoTT

IIUC the plan is indeed to take bits of everything. It just happens that @vbgl and @maximedenes wants to do this orderly and thought that ssreflect would be good for the very basic blocks. Please, let's not press them and let's not ask them to explain everything now, or else this is just going to block any kind of progress. Nonetheless, I still reiterate my very first comment in this PR: since this is a public repo, you need to put somewhere some information of what you expect from people at this stage.

Can we please have no canonical structures in stdlib2? I can think of perhaps 5 people who might understand how to debug or build stuff on top of these.

@vbgl and @maximedenes did try to use type-classes instead, and they found issues that they could not solve easily and that would require major redesign. So, even if they try to fix Coq whenever possible, this was too huge of a task in that case, and they took a pragmatic decision. Nonetheless, I agree that canonical structures are much harder to understand so this would deserve at least very good docs to compensate (and as little use of canonical structures as possible). For now, I only see one use of such canonical structure, and it is part of the lock pattern that was discussed above which, I guess, can be documented without needing to enter into the details of canonical structures.

gares · 2019-02-19T22:38:54Z

Can we please have no canonical structures in stdlib2? I can think of perhaps 5 people who might understand how to debug or build stuff on top of these.

I was quite impressed to see an effort by Maxime and Vincent rewrite a few layers of math-comp on top of type classes. I've always thought that TC and CS were equivalent in power, but the former seems to be more user friendly, so I was curious. The experiment failed, and Vincent gave a very detailed account of what does not work with TC, or better why the approach cannot scale. It is on youtube.

A library needs a retrofitting/inference mechanism, Coq has two of them, TC and CS. Since TC can't scale, the choice of CS seems inevitable to me. It would help to identify what makes CS less user friendly, so that we can improve on that.

I would love to have an actual discussion about modularity mechanisms, as I tried to start in #13.

Wrt #13 you point out two well know problematic approaches that are not followed by this PR (or math-comp). It is not easy to grasp the approach you propose, I'm sorry, but It seems Coq lacks some feature you need. You propose a hack (tile of your last commit) to implement your approach in the current system. Sorry to be that direct, but you don't base a standard library on a proof of concept. I'm all for understanding better your proposal, and it would help to have a summary/mock up in #13: pointers to commits are hard to understand, If you want comments you should make your proposal easy to find/read.

andres-erbsen · 2019-02-19T22:59:11Z

I responded at #13 (comment) I will refrain from commenting further until somebody posts what decisions input is accepted for, and what the outcomes of already finalized decisions are.

gmalecha · 2019-02-19T23:13:17Z

@gares is the link to the type classes / canonical structures video somewhere? I assume it was at a Coq working group, but which one?

Zimmi48 · 2019-02-19T23:27:32Z

https://www.youtube.com/watch?v=qoBC9Qo36FY

gmalecha · 2019-02-20T00:52:10Z

Thanks, @Zimmi48 . I realized that there is also a writeup of the results on the wiki.

Co-authored-by: Maxime Dénès <[email protected]> Co-authored-by: Vincent Laporte <[email protected]>

maximedenes · 2019-03-04T09:15:42Z

Thanks for the feedback. I think this can be merged now, and hopefully the global plan will become clearer in the next steps.

herbelin

Thanks for proposing this ssrbool-like contents to be part of a standard library. It is very comprehensive in the number of algebraic lemmas stated which is a very good point. We also know that it comes with a technology which has been proven useful for a number of applications (starting with the 4 color and Feit-Thompson theorems). In this sense, it deserves being carefully studied.

Looking at it, I have a first set of remarks and questions:

I'm unsure that the proving style parts should go in Bool.v (meaning here in particular the infrastructure for boolean reflection, such as if_spec, pred, the lock, ...). There are different proving styles, with different objectives, and I believe that the proving style techniques should go in a stand-alone specific library, with Bool require-able for all users without having to draw at the same time a proving infrastructure (several users made this request actually). For instance, pred is obviously the bool counterpart to Ensemble in Ensembles.v or unary_predicate in RelationClasses and both kinds of definitions should a priori be put into a similar perspective in a different library than Bool.v
I could not grasp at once the naming scheme, but this is interesting and I believe particularly interesting for intensive users knowing the names. On the other side, this might be frightening for new users. So, I can't stop believing that names should have synonyms, suitable to different levels of expertise. Said otherwise, a name like addKb looks more to me like an emacs key binding for a lemma name than like a lemma name properly. Common terminology and key bindings are both useful but none is universally better than the other.
I stopped today my reading at the definition of pred and I suspect that everything that comes from pred should go in another file.

As a matter of fact, the file is very large and my feeling is that it should be restricted to the algebraic properties over bool. In particular, I believe that we can get a consensus among different library developers on a unique library of Boolean algebraic properties, but I'm not convinced that we can as easily share proving styles based on bool with proving styles based on Prop. For the latter, one would probably need to provide different files in parallel, or, at best, to study what is common to the different styles.

In any cases, thanks a lot for bringing this file on the table so that a discussion can happen.

herbelin · 2020-04-04T14:29:29Z

src/bool.v

+
+Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" :=
+  (if c%bool is true as x in bool return t then v1 else v2) : boolean_if_scope.
+


What is the purpose of these notations? There is already a hard-wired syntax for if. Won't the above be more a source of confusion than doing some good?

herbelin · 2020-04-04T14:36:07Z

src/bool.v

+
+Reserved Notation "~~ b" (at level 35, right associativity).
+Reserved Notation "b ==> c" (at level 55, right associativity).
+Reserved Notation "b1  (+)  b2" (at level 50, left associativity).


The ==> and (+) look like good ideas. How used are there in practise in say MathComp?

One possible worry I see with ==> is that implb is not so common in boolean arithmetic, so it might hide a pretty convoited symbol. I'd be curious about feedback about its use.

I find ~~ pretty counterintuitive. Of cours, the rationale of doubling the symbol in notations over bool.v is a nice one, but in the case of negb, the collision with ~ ~ b, i.e. not (not b) seems worrying.

The notation (+) is not in the "doubled" style but intuitive. It might be convoited too, though.

herbelin · 2020-04-04T14:38:44Z

src/bool.v

+
+(**  Shorter delimiter  **)
+Local Delimit Scope bool_scope with B.
+Open Scope bool_scope.


Wouldn't it be disturbing to have two delimiters for bool_scope in a standard library (see coq/coq#11108 though). Why is the rationale for B? Is it just that it is shorter than bool?

herbelin · 2020-04-04T14:43:33Z

src/bool.v

+   [ do ![solve [trivial | apply: eq_sym; trivial]
+         | discriminate | contradiction | split]
+   | case not_locked_false_eq_true; assumption
+   | match goal with H : ~ _ |- _ => solve [case H; trivial] end ].


How does done compare to easy?

herbelin · 2020-04-04T14:47:59Z

src/bool.v

+Lemma negb_inj : injective negb. Proof. exact: can_inj negbK. Qed.
+Lemma negbLR b c : b = ~~ c -> ~~ b = c. Proof. exact: canLR negbK. Qed.
+Lemma negbRL b c : ~~ b = c -> b = ~~ c. Proof. exact: canRL negbK. Qed.
+


The short names look convenient for heavy users. How easy are the names to remember in practice? Can the names be derived relatively automatically from the statements?

herbelin · 2020-04-04T14:53:30Z

src/bool.v

+  | IfSpecFalse of  not_b : if_spec not_b false vF.
+
+Lemma ifP : if_spec (b = false) b (if b then vT else vF).
+Proof. by case def_b: b; constructor. Qed.


Looks interesting. How much is it about the bool structure vs about a "proof" technique which could be emphasized in a tactic library, or a tactic section of a bool directory?

herbelin · 2020-04-04T14:55:21Z

src/bool.v

+
+(**
+ Classical reasoning becomes directly accessible for any bool subgoal.
+ Note that we cannot use "unless" here for lack of universe polymorphism.    **)


Is this remark outdated?

herbelin · 2020-04-04T15:02:58Z

src/bool.v

+Notation "[ \/ P1 | P2 ]" := (or P1 P2) (only parsing) : type_scope.
+Notation "[ \/ P1 , P2 | P3 ]" := (or3 P1 P2 P3) : type_scope.
+Notation "[ \/ P1 , P2 , P3 | P4 ]" := (or4 P1 P2 P3 P4) : type_scope.
+


How much do these notations help in statements compared to nesting /\ and \/? If they help, why to stop at 5? More generally, if they help, doesn't this mean that we should support polymorphic families of inductive types (I guess ELPI could do the generation on demand of such andN and orN connectives?).

Shouldn't this be in a Logic file?

herbelin · 2020-04-04T15:03:55Z

src/bool.v

+
+Notation "[ || b1 | c ]" := (b1 || c) (only parsing) : bool_scope.
+Notation "[ || b1 , b2 , .. , bn | c ]" := (b1 || (b2 || .. (bn || c) .. ))
+  : bool_scope.


Is the purpose only to change associativity? Can you give examples of when this would be needed?

herbelin · 2020-04-04T15:06:27Z

src/bool.v

+Arguments norP [b1 b2].
+Arguments implyP [b1 b2].
+Prenex Implicits idP idPn negP negPn negPf.
+Prenex Implicits andP and3P and4P and5P orP or3P or4P nandP norP implyP.


Is it a form for which there is no Arguments equivalent syntax?

maximedenes approved these changes Feb 18, 2019

View reviewed changes

gmalecha reviewed Feb 18, 2019

View reviewed changes

SkySkimmer reviewed Feb 18, 2019

View reviewed changes

gares reviewed Feb 19, 2019

View reviewed changes

src/ssreflect.v Show resolved Hide resolved

gares reviewed Feb 19, 2019

View reviewed changes

src/ssreflect.v Outdated

].

(* Quicker done tactic not including split, syntax: /0/ *)

Ltac ssrdone0 :=

Copy link

Contributor

gares Feb 19, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

hem, yet another copy

andres-erbsen mentioned this pull request Feb 19, 2019

discussion of modularity mechanisms #13

Open

vbgl force-pushed the boot-stdlib2 branch from 242dc18 to 4d70445 Compare February 20, 2019 17:04

maximedenes and others added 2 commits February 28, 2019 08:58

Stdlib2: get started

54b3b3d

Co-authored-by: Maxime Dénès <[email protected]> Co-authored-by: Vincent Laporte <[email protected]>

Update README, adds CONTRIBUTING

43bd423

vbgl force-pushed the boot-stdlib2 branch from 4d70445 to 43bd423 Compare February 28, 2019 09:22

maximedenes merged commit c8b6606 into rocq-archive:master Mar 4, 2019

vbgl deleted the boot-stdlib2 branch March 4, 2019 09:17

herbelin reviewed Apr 4, 2020

View reviewed changes


		( #<style> .doc { font-family: monospace; white-space: pre; } </style># )

		Require Import functions.


		(** [option A] is the extension of [A] with an extra element [None] *)

		Variant option (A : Type) : Type :=


		Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" :=
		(if c%bool is true as x in bool return t then v1 else v2) : boolean_if_scope.

Stdlib2: get started #14

Stdlib2: get started #14

Conversation

vbgl commented Feb 18, 2019

Zimmi48 commented Feb 18, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

maximedenes Feb 18, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

herbelin commented Feb 19, 2019

maximedenes commented Feb 19, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

gmalecha commented Feb 19, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

gares commented Feb 19, 2019

gares commented Feb 19, 2019

herbelin commented Feb 19, 2019

herbelin commented Feb 19, 2019

Zimmi48 commented Feb 19, 2019

herbelin commented Feb 19, 2019

andres-erbsen commented Feb 19, 2019

Zimmi48 commented Feb 19, 2019

gares commented Feb 19, 2019

andres-erbsen commented Feb 19, 2019

gmalecha commented Feb 19, 2019

Zimmi48 commented Feb 19, 2019

gmalecha commented Feb 20, 2019

maximedenes commented Mar 4, 2019

herbelin left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

maximedenes Feb 18, 2019 •

edited

Loading