Topics:
- Converting `rel` to set function (3 messages, latest: Apr 18 2024 at 12:40)
- [coqeal] Getting plain `seq` from matrix (25 messages, latest: Apr 17 2024 at 11:12)
- Understanding coqeal example (3 messages, latest: Apr 10 2024 at 10:02)
- Specializing lemmas before using (8 messages, latest: Apr 10 2024 at 08:52)
- List utility functions (3 messages, latest: Apr 10 2024 at 08:43)
- A proof with {set unit} (5 messages, latest: Apr 08 2024 at 19:17)
- Set preimage proof (13 messages, latest: Apr 08 2024 at 18:12)
- Proof involving set equality (8 messages, latest: Apr 08 2024 at 10:09)
- Making a dependent type eqType (10 messages, latest: Apr 08 2024 at 05:05)
- MC2.1 substitution for bigmaxr (3 messages, latest: Apr 04 2024 at 19:00)
- Set to list conversion (5 messages, latest: Apr 03 2024 at 19:04)
- Filter {set A+B} to get {set A} (12 messages, latest: Apr 03 2024 at 07:01)
- Type matching between Reals and GRing.Zmodule (4 messages, latest: Mar 31 2024 at 13:37)
- Map a set (23 messages, latest: Mar 27 2024 at 09:17)
- 'Declaring' a type to be finite (5 messages, latest: Mar 26 2024 at 09:19)
- Destruct `predD` (4 messages, latest: Mar 26 2024 at 05:55)
- LeanSSR (11 messages, latest: Mar 23 2024 at 09:22)
- ✔ Goal with `\in` and seq (5 messages, latest: Mar 22 2024 at 09:30)
- Goal with `\in` and seq (1 message, latest: Mar 22 2024 at 06:40)
- Goal involving set intersection (4 messages, latest: Mar 21 2024 at 09:06)
- Type of powerset of a set (3 messages, latest: Mar 21 2024 at 08:25)
- ✔ Computing on code that uses views (1 message, latest: Mar 19 2024 at 16:47)
- Computing on code that uses views (3 messages, latest: Mar 19 2024 at 08:49)
- Converting `\in`-`pred` to function application (9 messages, latest: Mar 15 2024 at 17:17)
- Matrix Real Constants and Variables (7 messages, latest: Mar 04 2024 at 16:16)
- completeNormedModType of matrix (6 messages, latest: Feb 26 2024 at 18:31)
- Missing join of NormedZmodule and POrderZmodule (1 message, latest: Feb 26 2024 at 18:12)
- ✔ Syntax for reverse in multirule rewrite (2 messages, latest: Feb 26 2024 at 14:06)
- Syntax for reverse in multirule rewrite (9 messages, latest: Feb 26 2024 at 14:00)
- Canonical instance for finType of seq_sub (5 messages, latest: Feb 26 2024 at 12:19)
- R[i] is canonical to lmodType R by default? (3 messages, latest: Feb 26 2024 at 10:34)
- ✔ Canonical instance for finType of seq_sub (2 messages, latest: Feb 26 2024 at 08:20)
- n.+1 vs (n + 1) (8 messages, latest: Feb 22 2024 at 16:59)
- ✔ Using canonical instances in mathcomp2 (3 messages, latest: Feb 22 2024 at 12:00)
- SSProve in MC CI? (35 messages, latest: Feb 22 2024 at 09:22)
- Using canonical instances in mathcomp2 (11 messages, latest: Feb 22 2024 at 08:49)
- ✔ Using views (6 messages, latest: Feb 21 2024 at 06:51)
- ✔ all_ssreflect: Focusing on sub-goal (9 messages, latest: Feb 18 2024 at 10:50)
- How to define a lmod_porder Type with my_display (7 messages, latest: Feb 13 2024 at 18:42)
- ✔ cast in 'Z_p (4 messages, latest: Feb 13 2024 at 10:33)
- ✔ NIX CI testing with classical and analysis (1 message, latest: Feb 01 2024 at 23:16)
- NIX CI testing with classical and analysis (10 messages, latest: Feb 01 2024 at 17:20)
- MathComp 2.2.0 and 1.19.0 released (1 message, latest: Jan 18 2024 at 10:20)
- Useful lemmas about the free predicate? (12 messages, latest: Dec 14 2023 at 14:58)
- Presenting infinite monoids by generators and relations (1 message, latest: Dec 12 2023 at 14:33)
- ✔ Mixing MC 2.0 and MC 1.17 (1 message, latest: Dec 06 2023 at 11:27)
- Mixing MC 2.0 and MC 1.17 (4 messages, latest: Dec 06 2023 at 09:15)
- ✔ Examples for HB.instance using order.v (1 message, latest: Dec 04 2023 at 14:03)
- Examples for HB.instance using order.v (11 messages, latest: Dec 03 2023 at 12:49)
- Mathcomp 2.0 vs 1.18 (8 messages, latest: Nov 30 2023 at 16:23)
- ✔ Defining HB instance inside a proof. (1 message, latest: Nov 30 2023 at 15:02)
- Defining HB instance inside a proof. (7 messages, latest: Nov 30 2023 at 09:16)
- ✔ Linking order.v and 'I_n (1 message, latest: Nov 30 2023 at 09:10)
- Linking order.v and 'I_n (6 messages, latest: Nov 30 2023 at 08:59)
- Instance seem to be ignored. (16 messages, latest: Nov 29 2023 at 09:36)
- comoid from a zmodType (4 messages, latest: Nov 26 2023 at 07:26)
- ✔ ssreflect incompatible with analysis (2 messages, latest: Nov 23 2023 at 21:09)
- Building a comUnitRingType with Hierarchy Builder (7 messages, latest: Nov 23 2023 at 08:33)
- ssreflect incompatible with analysis (3 messages, latest: Nov 23 2023 at 00:05)
- Package pick ordering in Coq Platform (9 messages, latest: Nov 15 2023 at 11:04)
- getting started with fingroup (10 messages, latest: Nov 14 2023 at 08:17)
- ✔ best way to do powers in fingroup (1 message, latest: Nov 13 2023 at 21:51)
- best way to do powers in fingroup (3 messages, latest: Nov 13 2023 at 20:04)
- Where does the phrase "defective tactic" come from? (7 messages, latest: Nov 13 2023 at 07:14)
- Installation of mathcomp2 with 'make' (7 messages, latest: Nov 08 2023 at 06:00)
- Reshaping matrix (5 messages, latest: Oct 28 2023 at 18:51)
- A matrix mul proof (3 messages, latest: Oct 26 2023 at 12:14)
- proof involving \sum (9 messages, latest: Oct 25 2023 at 19:21)
- Few syntax doubts (3 messages, latest: Oct 23 2023 at 21:58)
- comSemiRing with bool (59 messages, latest: Oct 23 2023 at 14:53)
- Terence Tao is trying out Lean (7 messages, latest: Oct 21 2023 at 07:36)
- ✔ Problem installing odd-order with opam (2 messages, latest: Oct 19 2023 at 07:08)
- Problem installing odd-order with opam (7 messages, latest: Oct 18 2023 at 17:08)
- coqeal example (3 messages, latest: Oct 18 2023 at 14:33)
- Length of ord_enum list (44 messages, latest: Oct 18 2023 at 08:30)
- matrix multiplication (58 messages, latest: Oct 16 2023 at 17:58)
- ✔ Linear Algebra Basics (1 message, latest: Oct 15 2023 at 18:43)
- Installation of mathcomp2 (10 messages, latest: Oct 15 2023 at 17:34)
- Linear Algebra Basics (6 messages, latest: Oct 15 2023 at 16:53)
- ✔ Less verbose ssreflect proof (1 message, latest: Oct 14 2023 at 04:14)
- Less verbose ssreflect proof (7 messages, latest: Oct 13 2023 at 15:42)
- Matrix representation (49 messages, latest: Oct 12 2023 at 18:25)
- First element of a seq that fulfil a condition (12 messages, latest: Oct 11 2023 at 07:44)
- GenTree pedagogical example (7 messages, latest: Oct 05 2023 at 19:08)
- Meaning of `ChoiceType` (8 messages, latest: Oct 03 2023 at 18:21)
- mathcomp 2.0 status? (31 messages, latest: Sep 29 2023 at 11:48)
- Porting Deriving to math-comp 2.0.0 (17 messages, latest: Sep 29 2023 at 08:20)
- Finding the smallest structure with two properties (9 messages, latest: Sep 12 2023 at 14:02)
- choiceMixin (2 messages, latest: Sep 12 2023 at 13:45)
- native docker images? (1 message, latest: Sep 12 2023 at 01:10)
- ✔ negPf (5 messages, latest: Aug 29 2023 at 13:44)
- negPf (5 messages, latest: Aug 28 2023 at 08:14)
- computation with `exact:` (4 messages, latest: Aug 21 2023 at 14:51)
- tensors / multilinear maps (4 messages, latest: Aug 18 2023 at 20:26)
- Elliptic curves (23 messages, latest: Jul 14 2023 at 09:22)
- Code review (ordinal arithmetic) (6 messages, latest: Jul 09 2023 at 11:48)
- Isomorphism of finite groups (3 messages, latest: Jul 05 2023 at 07:21)
- Ring does not update its operations (18 messages, latest: Jun 30 2023 at 09:36)
- Mathcomp notation `{in [predC unit], _}` (8 messages, latest: Jun 26 2023 at 00:16)
- Best practices for automation in mathematical proofs (3 messages, latest: Jun 24 2023 at 20:24)
- Zₚ* cyclic (6 messages, latest: Jun 23 2023 at 10:11)
- Problem with exports in ssralg.v (22 messages, latest: Jun 22 2023 at 17:11)
- Problem with @Pack (11 messages, latest: Jun 19 2023 at 14:50)
- Tarjan 2.0 (14 messages, latest: Jun 19 2023 at 11:22)
- MathComp LOC (6 messages, latest: Jun 12 2023 at 11:01)
- Finite Types & Finite Graphs in MathComp (11 messages, latest: Jun 06 2023 at 11:43)
- Algebra tactics for stdlib fields (5 messages, latest: Jun 02 2023 at 07:22)
- Category Theory (25 messages, latest: May 23 2023 at 15:39)
- ✔ Semidirect Product (2 messages, latest: May 23 2023 at 13:43)
- Semidirect Product (14 messages, latest: May 22 2023 at 18:19)
- mczify for mathcomp 2.0 (4 messages, latest: May 15 2023 at 09:18)
- ✔ Hierarchy builder: two groups on the same type (5 messages, latest: May 14 2023 at 15:39)
- Hierarchy builder: two groups on the same type (3 messages, latest: May 14 2023 at 10:32)
- Can I compute with nat_of_ord? (1 message, latest: May 08 2023 at 19:08)
- ✔ Converting interval membership into comparisons (5 messages, latest: May 02 2023 at 09:40)
- Debugging auto (9 messages, latest: May 01 2023 at 14:59)
- ✔ why guard does not complain? (3 messages, latest: Apr 27 2023 at 21:07)
- independance of characters (2 messages, latest: Apr 27 2023 at 16:03)
- why guard does not complain? (3 messages, latest: Apr 27 2023 at 06:21)
- On-going migration of Docker mathcomp images infrastructure (1 message, latest: Apr 26 2023 at 20:51)
- Stuck with list membership (3 messages, latest: Apr 26 2023 at 08:22)
- degree 2 polynomials (1 message, latest: Apr 21 2023 at 14:06)
- ✔ Conversion 'I_p <-> 'Z_p (2 messages, latest: Apr 14 2023 at 07:36)
- coq-interval but for integers (8 messages, latest: Apr 13 2023 at 14:57)
- Conversion 'I_p <-> 'Z_p (4 messages, latest: Apr 12 2023 at 19:11)
- Surjectivity (6 messages, latest: Apr 12 2023 at 08:58)
- under tactic with setoid rewrite (15 messages, latest: Apr 08 2023 at 08:31)
- Using auto with mathcomp (14 messages, latest: Apr 07 2023 at 00:19)
- Code review - new user (3 messages, latest: Apr 06 2023 at 14:12)
- ✔ Calculating in Zmodp (9 messages, latest: Apr 05 2023 at 14:03)
- Calculating in Zmodp (12 messages, latest: Apr 05 2023 at 09:54)
- ✔ Windows mathcomp version (2 messages, latest: Mar 30 2023 at 13:43)
- Windows mathcomp version (3 messages, latest: Mar 30 2023 at 12:51)
- Printing finmap's allpairs forgets notation (1 message, latest: Mar 28 2023 at 17:03)
- ✔ have with inductive spec (3 messages, latest: Mar 23 2023 at 17:30)
- arg min (29 messages, latest: Mar 16 2023 at 23:47)
- Cycles (10 messages, latest: Mar 13 2023 at 23:34)
- Understanding extremum_spec (4 messages, latest: Mar 11 2023 at 19:43)
- Learning finite fields with mathcomp (12 messages, latest: Mar 03 2023 at 16:36)
- Two versions of the same data structure (14 messages, latest: Feb 27 2023 at 02:28)
- Notation for composing functions (25 messages, latest: Feb 25 2023 at 07:19)
- and3 (14 messages, latest: Feb 23 2023 at 22:24)
- Coq not computing catf (7 messages, latest: Feb 23 2023 at 21:58)
- ✔ eq_refl (5 messages, latest: Feb 22 2023 at 17:37)
- ✔ Using the under tactic (5 messages, latest: Feb 21 2023 at 20:29)
- Composition of fmaps (1 message, latest: Feb 19 2023 at 04:07)
- ✔ Bigop sum of types (8 messages, latest: Feb 15 2023 at 19:30)
- How to go from `Prop` to `bool` (and get proof irrel.) (32 messages, latest: Feb 14 2023 at 09:44)
- ✔ [forall _, true] doesn't eval to true (25 messages, latest: Feb 13 2023 at 03:59)
- ✔ rewrite -deprecated_filter_index_enum (4 messages, latest: Feb 11 2023 at 07:56)
- ✔ Shared domain of fmaps (70 messages, latest: Feb 10 2023 at 19:51)
- Square root on ereals (1 message, latest: Feb 10 2023 at 14:40)
- coqeal (55 messages, latest: Feb 10 2023 at 12:52)
- surjective functions (26 messages, latest: Jan 30 2023 at 14:26)
- How to do a rewrite between an elim and introducting IH (18 messages, latest: Jan 27 2023 at 10:09)
- ✔ Rewrite in existential (5 messages, latest: Jan 24 2023 at 03:00)
- ✔ Error: ssr_have was not found in the current environment (2 messages, latest: Jan 20 2023 at 11:25)
- ✔ Different representations for elements of finsets (10 messages, latest: Jan 19 2023 at 21:54)
- Explicit construction of F256 (27 messages, latest: Jan 19 2023 at 17:29)
- should we expect mc2.0 any time soon? (8 messages, latest: Jan 19 2023 at 12:39)
- Proving [fset x | x in A & x \in B] = B (4 messages, latest: Jan 16 2023 at 21:53)
- has vs exists (15 messages, latest: Jan 16 2023 at 10:03)
- Automation tools (16 messages, latest: Jan 13 2023 at 16:13)
- Documentation and tutorial for finmap and finset (3 messages, latest: Jan 12 2023 at 04:02)
- case-analysis on element of union of finite sets (9 messages, latest: Jan 05 2023 at 03:02)
- simpl vs cbn (52 messages, latest: Dec 17 2022 at 20:57)
- MC School 2022 material (3 messages, latest: Dec 15 2022 at 21:52)
- ✔ How to install MC2.0 alpha via opam while it is pre-re... (2 messages, latest: Dec 15 2022 at 16:30)
- ✔ docker / mc 1.15 / coq dev (5 messages, latest: Nov 28 2022 at 14:31)
- Proof of codomf_set (21 messages, latest: Nov 25 2022 at 15:43)
- ✔ Beta-reduction of finite function (5 messages, latest: Nov 25 2022 at 15:20)
- What would be mathcomp eqiivalent of decidable Prop? (1 message, latest: Nov 19 2022 at 09:52)
- Missing coercion from {fset C} to finType (16 messages, latest: Nov 18 2022 at 18:48)
- Math Comp Workshop December 2022 (9 messages, latest: Nov 18 2022 at 18:18)
- How to automate inheriting two canonical structures ? (12 messages, latest: Nov 17 2022 at 23:06)
- view to transform nested [forall x, forall y, ...] (7 messages, latest: Nov 16 2022 at 00:56)
- ✔ Non-instantiated existential variables (41 messages, latest: Nov 15 2022 at 06:04)
- Does mathcomp has notion of seq permutation without EqType (46 messages, latest: Nov 14 2022 at 20:11)
- ✔ Empty finType (37 messages, latest: Nov 14 2022 at 00:20)
- ✔ Rewrite with ring (7 messages, latest: Nov 11 2022 at 15:39)
- How to discharge annoying dis-equality patterns (13 messages, latest: Nov 11 2022 at 14:03)
- Output not accepted as input (15 messages, latest: Nov 08 2022 at 10:25)
- Is there inversion and general induction in mathcomp ? (18 messages, latest: Nov 08 2022 at 10:22)
- ✔ How to destruct a non existent mathcomp equality. (8 messages, latest: Nov 07 2022 at 21:27)
- ✔ What is this notation (5 messages, latest: Nov 07 2022 at 08:27)
- ✔ how to do remember ... as (3 messages, latest: Nov 05 2022 at 13:09)
- Fold lemmas (2 messages, latest: Nov 04 2022 at 15:45)
- ✔ Instantiate [exists _, _] (6 messages, latest: Nov 04 2022 at 11:35)
- ✔ `apply` works but `apply : ` fails (7 messages, latest: Nov 04 2022 at 10:18)
- ✔ ssreflect unfold `In` but I don't want it to? (17 messages, latest: Nov 03 2022 at 16:30)
- ✔ finType and card (16 messages, latest: Nov 03 2022 at 16:30)
- ✔ countType vs choiceType (4 messages, latest: Nov 03 2022 at 16:27)
- Request for Comments/ Code review (32 messages, latest: Nov 03 2022 at 13:04)
- Question abount finType (6 messages, latest: Nov 02 2022 at 00:56)
- RFC ssrmap (4 messages, latest: Nov 01 2022 at 16:41)
- Stuck at finType and \sum_ (5 messages, latest: Oct 29 2022 at 16:02)
- Struggle with using canonical structures mathcomp style (1 message, latest: Oct 28 2022 at 17:58)
- Why doesn't math-comp use cool notation (40 messages, latest: Oct 27 2022 at 23:07)
- ✔ stuck at finding good relation between \in and \notin (4 messages, latest: Oct 26 2022 at 15:13)
- could not fill dependent hole in "apply" (6 messages, latest: Oct 25 2022 at 21:02)
- What is the problem with `seq A` if just has `EqType`? (9 messages, latest: Oct 25 2022 at 14:18)
- The equivalent of auto in ssreflect (11 messages, latest: Oct 24 2022 at 09:17)
- Rewrite doesn't see subterms (6 messages, latest: Oct 20 2022 at 11:07)
- ssrnat: missing lemma? (7 messages, latest: Oct 19 2022 at 17:02)
- finType and Variant (15 messages, latest: Oct 19 2022 at 12:02)
- ssr and Coq bullets (3 messages, latest: Oct 13 2022 at 08:35)
- ✔ Nonincreasing sequences: one step is equivalent to global (10 messages, latest: Oct 11 2022 at 15:05)
- ✔ Lemma comparing leq and addn: missing or not found? (6 messages, latest: Oct 11 2022 at 13:12)
- ✔ Double induction (5 messages, latest: Oct 02 2022 at 07:07)
- ✔ measure ssrnat (8 messages, latest: Oct 01 2022 at 20:09)
- ✔ What is the benefits of small-scale reflection? (9 messages, latest: Sep 24 2022 at 03:03)
- Failure trying to use telescope_sumr (32 messages, latest: Sep 23 2022 at 08:39)
- ✔ Failing with hornerE (5 messages, latest: Sep 20 2022 at 22:25)
- Questions on matching (2 messages, latest: Sep 10 2022 at 03:17)
- Unlock finfuns (8 messages, latest: Sep 09 2022 at 18:42)
- `rewrite /` and $$\zeta$$-reduction (13 messages, latest: Sep 08 2022 at 13:42)
- ✔ Concise way to rewrite without intro & revert back? (14 messages, latest: Sep 08 2022 at 12:11)
- ✔ Tactics for solving GRing equations? (10 messages, latest: Sep 08 2022 at 04:48)
- hammer (61 messages, latest: Sep 07 2022 at 04:24)
- ✔ Definition of \sum_i \sum_j \sum_k... (6 messages, latest: Sep 05 2022 at 20:17)
- ✔ Cannot use existing linear structure of `\- u` (4 messages, latest: Sep 05 2022 at 14:34)
- ✔ Way to make sense of phantoms (and mixins) (13 messages, latest: Sep 04 2022 at 08:18)
- ✔ Got `_m_` while eliminating inductive proposition (4 messages, latest: Sep 02 2022 at 03:14)
- ✔ Are inductive propositions unidiomatic in ssreflect? (8 messages, latest: Sep 02 2022 at 00:59)
- ✔ Proving linearity is closed on function add/scale (8 messages, latest: Aug 25 2022 at 01:00)
- ✔ How to use subtype mixins? (25 messages, latest: Aug 23 2022 at 14:28)
- ✔ Formal note-taking on "Introduction to Manifold" (2 messages, latest: Aug 20 2022 at 08:02)
- ✔ Documentation of math-comp Search (4 messages, latest: Aug 13 2022 at 09:04)
- ✔ sigma type from exists (5 messages, latest: Aug 08 2022 at 23:15)
- ✔ Dependent types: total functions from #|[set w | P w]|=1 (7 messages, latest: Aug 06 2022 at 11:06)
- [Complete beginner] Trying out math-comp (87 messages, latest: Jul 27 2022 at 19:29)
- Transfer of structure for ordered types (3 messages, latest: Jul 26 2022 at 09:38)
- S n' not the same as n' .+1? (11 messages, latest: Jul 22 2022 at 08:21)
- Are ssreflect-only questions appropriate here (2 messages, latest: Jul 21 2022 at 17:19)
- Quotients (39 messages, latest: Jul 08 2022 at 23:56)
- Coq Platform 8.16 preview release (43 messages, latest: Jun 25 2022 at 07:56)
- ✔ Implement lexical order (3 messages, latest: Jun 22 2022 at 09:40)
- Makefile license (3 messages, latest: Jun 15 2022 at 14:37)
- Missing notations with reals? (3 messages, latest: Jun 13 2022 at 06:49)
- Declaring dual structure (1 message, latest: Jun 08 2022 at 10:20)
- Utility library coordination (12 messages, latest: Jun 06 2022 at 18:16)
- Coq-combi (5 messages, latest: Jun 06 2022 at 16:53)
- "An Introduction to Small-Scale Reflection in Coq" (7 messages, latest: Jun 03 2022 at 02:30)
- ✔ Unicity of prime decomposition (20 messages, latest: May 31 2022 at 09:49)
- ✔ Proof about \big and List.fold_left (4 messages, latest: May 26 2022 at 08:05)
- ✔ Awful proof on rationals (8 messages, latest: May 25 2022 at 20:25)
- "unpacking" Choice.sort (23 messages, latest: May 24 2022 at 13:24)
- ✔ Polynomials with multiple variables (4 messages, latest: May 23 2022 at 13:03)
- ✔ Converting Coq (normal) Field Type to math-comp fieldType (9 messages, latest: May 21 2022 at 12:09)
- Polynomials (6 messages, latest: May 20 2022 at 13:03)
- ✔ Complex numbers (15 messages, latest: May 18 2022 at 16:28)
- ✔ How to use x - x = 0 in a ring ? (7 messages, latest: May 17 2022 at 05:03)
- ✔ Proving that functions are inverse of each other (13 messages, latest: May 13 2022 at 23:40)
- vectType of functions (4 messages, latest: May 10 2022 at 12:35)
- ✔ Simplifying matrix_of_fun_def (7 messages, latest: May 09 2022 at 20:15)
- \max with order.v (2 messages, latest: May 09 2022 at 14:30)
- Relating eigenvalue definition from mathcomp and Jordan form (20 messages, latest: May 09 2022 at 12:55)
- Group theory related theorem proving by coq. (2 messages, latest: May 06 2022 at 12:48)
- ✔ have [] and case (4 messages, latest: May 04 2022 at 23:44)
- stream events (7 messages, latest: May 04 2022 at 07:50)
- About vectType (5 messages, latest: May 03 2022 at 14:25)
- `perm_eq` for swap (6 messages, latest: May 01 2022 at 19:00)
- field/nsatz tactic with ZmodP (13 messages, latest: Apr 20 2022 at 18:45)
- \max with orderType (5 messages, latest: Apr 18 2022 at 18:19)
- \min (10 messages, latest: Apr 07 2022 at 13:14)
- [finmap] `fset_finpred` vs `fin_finpred` (2 messages, latest: Apr 06 2022 at 12:19)
- Basic Use of Mathcomp and Opacity (6 messages, latest: Apr 05 2022 at 06:27)
- SSreflect case (9 messages, latest: Apr 01 2022 at 18:20)
- split on membership in list (1 message, latest: Apr 01 2022 at 15:04)
- Hierarchy builder error (1 message, latest: Mar 25 2022 at 13:47)
- duplicate clear (18 messages, latest: Mar 14 2022 at 19:39)
- ✔ homo typechecking (5 messages, latest: Mar 13 2022 at 18:42)
- Require Import mathcomp.ssreflect.ssreflect. (19 messages, latest: Mar 11 2022 at 20:05)
- Decide Equality ? (12 messages, latest: Mar 10 2022 at 15:07)
- Coq Prime (3 messages, latest: Mar 09 2022 at 09:30)
- Monotonicity lemmas' names for nat (3 messages, latest: Mar 06 2022 at 21:27)
- Notation inconsistency : `_.[_ <- _]` (3 messages, latest: Feb 24 2022 at 13:07)
- Implementing SHA256 in MathComp (34 messages, latest: Feb 22 2022 at 12:54)
- ✔ From mathcomp Require Import all -- not working? (23 messages, latest: Feb 19 2022 at 09:24)
- Vector spaces -- not finite dimensional (11 messages, latest: Feb 14 2022 at 10:06)
- Wordle in MathComp (1 message, latest: Feb 10 2022 at 19:41)
- ✔ wrong display of list membership (7 messages, latest: Feb 10 2022 at 10:04)
- Little porting puzzle (7 messages, latest: Feb 06 2022 at 08:48)
- Templates for Apery (26 messages, latest: Feb 04 2022 at 10:27)
- induced matrix norms (1 message, latest: Feb 03 2022 at 18:16)
- Newton-Girard identities (2 messages, latest: Feb 02 2022 at 09:05)
- representation of a vector in terms of basis (6 messages, latest: Jan 29 2022 at 19:39)
- ✔ recursive function adn typechecing (5 messages, latest: Jan 29 2022 at 10:43)
- ✔ Missing logic lemma? (5 messages, latest: Jan 27 2022 at 08:50)
- 8.15 pick for Coq Platform (7 messages, latest: Jan 25 2022 at 18:05)
- Depending on core MathComp opam packages (2 messages, latest: Jan 24 2022 at 16:04)
- Canonical structure creation warning (8 messages, latest: Jan 24 2022 at 15:30)
- Compatibility testing MC+Coq (3 messages, latest: Jan 23 2022 at 23:00)
- ✔ Evaluating option values (10 messages, latest: Jan 23 2022 at 13:15)
- MathComp 1.14.0 released (1 message, latest: Jan 19 2022 at 12:15)
- Implementing alternative TC resolution in a plugin (35 messages, latest: Jan 16 2022 at 12:57)
- SSR/MathComp Lectures (5 messages, latest: Jan 14 2022 at 15:18)
- Measuring gains from using small-scale reflection (32 messages, latest: Jan 14 2022 at 13:09)
- Limitations of MathComp ambient structures (11 messages, latest: Jan 13 2022 at 15:36)
- Release of MC 1.14 (1 message, latest: Jan 12 2022 at 09:34)
- equivalence classes of fingraph (3 messages, latest: Jan 08 2022 at 14:55)
- OrdinalOrder (6 messages, latest: Dec 22 2021 at 20:32)
- Coercion issue (4 messages, latest: Dec 15 2021 at 13:40)
- Hint databases for finishing tactic (24 messages, latest: Dec 14 2021 at 14:16)
- Array definition fails (2 messages, latest: Dec 09 2021 at 19:50)
- how to prove symmetry of [pred x | p1 x == p2 x]? (3 messages, latest: Nov 29 2021 at 10:28)
- ✔ case_eq in SSR style (6 messages, latest: Nov 24 2021 at 08:20)
- Term selection under norm (11 messages, latest: Nov 23 2021 at 11:33)
- Hierachy Builder talk (2 messages, latest: Nov 19 2021 at 12:37)
- ✔ working with `{in _ _}` (13 messages, latest: Nov 18 2021 at 01:06)
- how to create =i equality (7 messages, latest: Nov 16 2021 at 06:59)
- `finmap`: rewriting `{fset K}` membership (5 messages, latest: Nov 15 2021 at 15:55)
- Coq Platform 2021.11 preparation (6 messages, latest: Nov 15 2021 at 13:16)
- naming convention (24 messages, latest: Nov 15 2021 at 11:53)
- ✔ how to work with `mem`? (6 messages, latest: Nov 15 2021 at 07:50)
- ✔ how to work with all (fun x => has (pred1 x) s1) s2 (14 messages, latest: Nov 14 2021 at 17:15)
- ✔ how ot use =i? in example undup s i= s (5 messages, latest: Nov 13 2021 at 23:18)
- ✔ how to prove x \in s -> x \in s++s' ? (14 messages, latest: Nov 13 2021 at 23:18)
- countType in finmap (12 messages, latest: Nov 13 2021 at 21:13)
- fold property in a sum using bigop (7 messages, latest: Nov 10 2021 at 17:29)
- mathcomp analysis summation proof help (16 messages, latest: Nov 10 2021 at 17:22)
- Proofs about pi (7 messages, latest: Nov 03 2021 at 12:26)
- MathComp 1.13.0 released (7 messages, latest: Nov 01 2021 at 09:16)
- topological sorting in mathcomp (50 messages, latest: Oct 30 2021 at 18:25)
- refinement between rel T and T -> seq T (9 messages, latest: Oct 27 2021 at 08:37)
- Complex number equality (8 messages, latest: Oct 26 2021 at 14:10)
- extra-dev constraints for fcsl-pcm (5 messages, latest: Oct 26 2021 at 12:15)
- Default subscribed streams (1 message, latest: Oct 24 2021 at 20:34)
- citing mathcomp (5 messages, latest: Oct 22 2021 at 16:41)
- Towards a CEP for improving Search (1 message, latest: Oct 22 2021 at 09:27)
- Generating rewrite directives out of ring or field tactic... (18 messages, latest: Oct 21 2021 at 15:23)
- how to restore information after building a tuple (6 messages, latest: Oct 21 2021 at 13:12)
- hnf & discriminate (17 messages, latest: Oct 20 2021 at 10:09)
- how to combine two top assumptions with `conj` (36 messages, latest: Oct 19 2021 at 21:41)
- build verified boolean formula solver (24 messages, latest: Oct 18 2021 at 10:21)
- create finType from unique seq (40 messages, latest: Oct 15 2021 at 10:27)
- Order on {set T} (6 messages, latest: Oct 01 2021 at 20:45)
- rank type (1 message, latest: Oct 01 2021 at 15:42)
- \max in order.v (3 messages, latest: Oct 01 2021 at 15:11)
- row_free vs free (4 messages, latest: Oct 01 2021 at 13:06)
- Removal of ssrsearch (6 messages, latest: Sep 24 2021 at 10:43)
- under rewriting (23 messages, latest: Sep 17 2021 at 14:45)
- 0.+1 (4 messages, latest: Sep 17 2021 at 09:39)
- Best practice : keeping tests (6 messages, latest: Sep 14 2021 at 23:12)
- monotonicity of (n/(n+1))^(n+1) (21 messages, latest: Sep 08 2021 at 11:43)
- Matrix canonical forms repo (4 messages, latest: Sep 07 2021 at 18:05)
- expanding a matrix multiplication (12 messages, latest: Aug 30 2021 at 07:52)
- tval tcast (2 messages, latest: Aug 26 2021 at 19:21)
- Splitting bigop on a predicate, and even/odd expansion (20 messages, latest: Aug 26 2021 at 13:44)
- perm_eq for equal seqs (17 messages, latest: Aug 20 2021 at 12:13)
- Ring Quotient Error (3 messages, latest: Aug 14 2021 at 13:36)
- automatic rewriting of linear equations (6 messages, latest: Jul 26 2021 at 13:31)
- 1.13 ? (4 messages, latest: Jul 07 2021 at 14:23)
- Order of multiple views in apply (1 message, latest: Jun 17 2021 at 14:54)
- val/tval handling (5 messages, latest: Jun 13 2021 at 10:38)
- \near x, something true (1 message, latest: Jun 01 2021 at 14:17)
- Getting started with mathcomp-analysis : continuo... (1 message, latest: Jun 01 2021 at 10:09)
- Using natmul_continuous on the support realType (1 message, latest: Jun 01 2021 at 10:08)
- Problem of extensionality in filters (1 message, latest: Jun 01 2021 at 10:08)
- norm and multiplication (4 messages, latest: May 31 2021 at 15:58)
- line endings? (2 messages, latest: May 27 2021 at 21:48)
- Use ring tactic on int (17 messages, latest: May 21 2021 at 21:21)
- revert/move (4 messages, latest: May 19 2021 at 13:53)
- Mapping a polynomial to the sequence of its roots (1 message, latest: May 19 2021 at 12:47)
- Getting rid of ... \is Num.pos (4 messages, latest: May 19 2021 at 12:42)
- have an typeclasses (3 messages, latest: May 17 2021 at 21:35)
- Learning bigop ? (22 messages, latest: May 12 2021 at 12:58)
- quaternions (4 messages, latest: Apr 28 2021 at 11:48)
- case on a type family with 2 indices (5 messages, latest: Apr 27 2021 at 20:48)
- Question on Num.RealField (15 messages, latest: Apr 23 2021 at 15:23)
- A question on fset (32 messages, latest: Apr 19 2021 at 16:33)
- Cases modulo n (10 messages, latest: Apr 16 2021 at 10:07)
- Question on ssralg (2 messages, latest: Apr 14 2021 at 16:22)
- MathComp for HoTT? (26 messages, latest: Apr 14 2021 at 12:54)
- m %% 0 = m (5 messages, latest: Apr 08 2021 at 14:54)
- reversing the tactic apply : (iffP idP) (3 messages, latest: Apr 07 2021 at 07:13)
- complain about order of arguments of mulrBl (1 message, latest: Mar 30 2021 at 15:36)
- Ways to dispose of hypotheses (7 messages, latest: Mar 26 2021 at 20:38)
- Finmap construction (13 messages, latest: Mar 25 2021 at 15:06)
- partitions (7 messages, latest: Mar 15 2021 at 17:24)
- Idiom with nth_error (7 messages, latest: Mar 12 2021 at 18:45)
- identify math-comp version? (6 messages, latest: Mar 05 2021 at 12:52)
- finfun / dfinfun (8 messages, latest: Mar 02 2021 at 10:45)
- Performance when computing with finmap (3 messages, latest: Feb 24 2021 at 16:33)
- ssrint (10 messages, latest: Feb 18 2021 at 22:03)
- finmap and key (55 messages, latest: Feb 06 2021 at 11:07)
- Installation fails (1.12.0, coq-8.13, CYGWIN, ocaml-mingw64) (10 messages, latest: Feb 05 2021 at 14:52)
- obtaining countability from finiteness (3 messages, latest: Jan 29 2021 at 19:13)
- Documenting mathcomp theorems (26 messages, latest: Jan 27 2021 at 14:27)
- Important theorems about linear algebra? (5 messages, latest: Jan 27 2021 at 14:23)
- A formal proof of Abel-Ruffini Theorem in Coq (16 messages, latest: Jan 27 2021 at 13:25)
- FreeModules (4 messages, latest: Jan 05 2021 at 19:15)
- finmaps and universes (17 messages, latest: Dec 19 2020 at 15:52)
- Idiom with have? (14 messages, latest: Dec 14 2020 at 15:20)
- Exporting of notations in ssrfun.v (3 messages, latest: Dec 07 2020 at 14:57)
- GitHub topic for mathcomp (21 messages, latest: Dec 07 2020 at 11:10)
- Deriving instances (7 messages, latest: Dec 03 2020 at 14:16)
- Induction & counting with ordinals (5 messages, latest: Dec 02 2020 at 16:18)
- finmap: Canonical choiceType for {fset K} (23 messages, latest: Nov 27 2020 at 13:21)
- MathComp 1.12.0 released (23 messages, latest: Nov 26 2020 at 11:48)
- Induction on size of finite set (28 messages, latest: Nov 17 2020 at 12:41)
- Adding mathcomp tag to GitHub projects (2 messages, latest: Nov 08 2020 at 00:23)
- Working with relative integers (7 messages, latest: Nov 04 2020 at 22:35)
- ring theory in mathcomp (23 messages, latest: Oct 25 2020 at 19:57)
- Nix for mathcomp (36 messages, latest: Oct 25 2020 at 12:55)
- Equality of dffun (3 messages, latest: Oct 25 2020 at 12:03)
- bigop convert range to ordinal (20 messages, latest: Oct 23 2020 at 16:01)
- sumbool_of_bool in math-comp? (15 messages, latest: Oct 19 2020 at 16:35)
- computing variant of `ord_enum` (7 messages, latest: Oct 13 2020 at 16:28)
- Surprising parsing of the “*l” notation (10 messages, latest: Oct 09 2020 at 17:01)
- viewer <> as != in a goal ? (9 messages, latest: Oct 04 2020 at 15:53)
- How to use bigop results for different ranges (32 messages, latest: Sep 30 2020 at 15:43)
- equation manipulation (12 messages, latest: Sep 28 2020 at 10:48)
- mczify (13 messages, latest: Sep 28 2020 at 08:30)
- Developing basic (modern) algebraic geometry in mathcomp (18 messages, latest: Sep 22 2020 at 09:11)
- using finmap (5 messages, latest: Sep 02 2020 at 10:37)
- MathComp as an "evolving foundational text" (5 messages, latest: Sep 02 2020 at 10:36)
- ring_scope and nat notations (2 messages, latest: Aug 19 2020 at 11:40)
- which opam packages correspond to configure+install (35 messages, latest: Aug 17 2020 at 10:40)
- Encapsulation for finmap with default value? (13 messages, latest: Aug 11 2020 at 12:41)
- Bigop and the direct sum of modules (10 messages, latest: Jul 31 2020 at 13:07)
- from telescopes to packaged structures (13 messages, latest: Jul 20 2020 at 15:57)
- Best way to include mathcomp without the tactic language (6 messages, latest: Jul 13 2020 at 16:52)
- Citing math-comp (6 messages, latest: Jul 12 2020 at 18:03)
- A question about finType (21 messages, latest: Jul 09 2020 at 06:41)
- How to use finset (74 messages, latest: Jul 08 2020 at 20:23)
- MathComp 1.11.0 released (3 messages, latest: Jun 09 2020 at 18:17)
- MathComp 1.11.0 OPAM packages Coq compatibility (1 message, latest: Jun 09 2020 at 14:58)
- Release of machine learning dataset based on MC 1.9.0 (2 messages, latest: Jun 05 2020 at 07:02)
- finmap-1.4.0 incompatibility with Coq 8.11.1 (45 messages, latest: Jun 03 2020 at 12:56)
- finmap-order (8 messages, latest: Jun 02 2020 at 20:06)
- graph algorithms in Graph Theory project (6 messages, latest: Jun 02 2020 at 18:20)
- infinitude of primes via reglang? (3 messages, latest: May 25 2020 at 19:17)
- [Crosspost] Issue 436 (call for PRs) (1 message, latest: May 21 2020 at 14:50)
- induction lemmas (2 messages, latest: May 11 2020 at 10:48)
- code conventions (2 messages, latest: May 08 2020 at 11:42)
- imported from gitter room math-comp/Lobby (864 messages, latest: Apr 22 2020 at 14:11)
Last updated: Apr 19 2024 at 02:02 UTC