Christian Doczkal
Christian Doczkal
I noticed that there are some strange statement/naming inconsistencies in `ssrnat.v` ```coq leq_addr: forall m n : nat, n m < n + p ``` besides the fact that these...
I just noticed that the definitions of `closed_mem e` and `closure_mem e` are only meaningful if `connect_sym e` holds (in the sense that `closure_closed` has `connect_sym e` as an assumption)....
##### Motivation for this change Adapt the definitions of `closed` and `closure` so that they apply to general relations (i.e., those for which `connect_sym` does not hold. Resolves #466 Observation:...
I noticed (actually quite a while ago) that there are two related and not particularly well-developed notions in the library: `n_comp` and `partition` (in particular the `equivalence_partition`). They differ significantly...
As part of the discussion of PR #632 , it was noted that the absence of list membership for lists over types without a decidable equality (no `eqType` instance) may...
Being a frequent user of `contra_` lemmas I wonder whether there would be a way to avoid having a separate lemma for every combination of (decidable) predicates (cf. #578), and...
I just proved a number of additional results on `subseq`, `next`, `arc`, and `findex`. It's a bit long to post here in it's entirety, but maybe some of these could...
In a recent development we used big operators in a context where we only had a (commutative) monoid up to some equivalence relation. As a consequence, I ended up porting...
In my opinion, the default configuration of ProofGeneral/EasyCrypt has several shortcomings, that should all be easy to fix: - [ ] `electric-indent-mode` is enabled by default and IMHO less than...
For testing purposes, I was trying to get `easycrypt-mode` to use a different easycrypt binary than the one that's in the PATH as `"easycrypt"` (which is the sensible default value...