Andres Erbsen
Andres Erbsen
bedrock2, rupicola, and fiat-crypto primarily use LittleEndianList after https://github.com/mit-plv/fiat-crypto/pull/1085/files ; there is still some LittleEndian in the bedrock2 compiler and more in riscv-coq.
Merged, thanks!
Trickling down at https://github.com/mit-plv/bedrock2/pull/153 ...
FixCoqMistakes sounds like https://github.com/mit-plv/coqutil/blob/master/src/coqutil/sanity.v https://coq.inria.fr/refman/changes.html > Changed: The default tactic used by firstorder is auto with core instead of auto with *; see Solvers for logic and equality for details;...
:/. having never used ocaml extraction, I don't know what to look at here
is there a reason not to put that directive right after the definition?
This is a cool contribution -- please don't take my tardiness in tending to it as a negative judgement. I flipped through the code, found it reasonable, and prepared a...
@gares https://github.com/coq/stdlib2/pull/14#issuecomment-465340287 how do canonical structures solve these issues? For example, would a well-written tactic that works on semirings defined using canonical structures work on a goal that uses nat...
Wow, it does look like canonical structures avoid the issues I brought up for typeclasses. Is there a way to trigger the same matching directly without calling rewrite (e.g. as...
This sounds great. I would propose to systematically rule out use of `auto with *` using something like [this](https://github.com/mit-plv/fiat-crypto/blob/master/src/Util/FixCoqMistakes.v) ~~~~~ (** [intuition] means [intuition auto with *]. This is very...