KimayaBedarkar

Indentation issue : "\in"

2

SSReflect uses `\in` as opposed to the unicode `∈` to indicate membership in lists. However, the former is not indented correctly. Example: ``` Lemma test: forall a : nat, a...

change the implicit arguments of big cat nat

2

##### Motivation for this change The current way arguments for the lemma `big_cat_nat` are declared makes it hard to use the lemma in developments. This MR changes the arguments that...

Document global flags set by mathcomp

1

Mathcomp changes some default coq behaviors globally by setting some flags. Examples: https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssreflect.v#L5-L6 These global behaviors are inherited by any project that imports mathcomp. So, these flags having global effects...

I tried installing z3 (version 4.14.1) via the opam package manager. I am on MacOS 15.4 + arm64. The opam switch that I am in has a name that is...