StackExchange Bot (Jun 24 2020 at 20:48): StackExchange Bot (Jun 24 2020 at 20:48):Feryll posted a new question on June 24, 2020 at 10:39PM: A suitably polymorphic definition of commutation in Coq – stackoverflow.com
StackExchange Bot (Jun 24 2020 at 21:48):Feryll posted a new question on June 24, 2020 at 11:34PM: Instantiating a class with a sig'd type in Coq – cs.stackexchange.com
StackExchange Bot (Jun 25 2020 at 12:48):rosi javi posted a new question on June 25, 2020 at 02:20PM: How to simplify lemma – stackoverflow.com
StackExchange Bot (Jun 26 2020 at 14:48):Max Heiber posted a new question on June 26, 2020 at 04:39PM: Does Gallina have an equivalent of Haskell's $ or Ocaml's @@ – stackoverflow.com
StackExchange Bot (Jun 26 2020 at 17:48):Carl Patenaude Poulin posted a new question on June 26, 2020 at 07:40PM: Simple syntax for terms of decidable subset types – stackoverflow.com
StackExchange Bot (Jun 26 2020 at 17:48):Carl Patenaude Poulin posted a new question on June 26, 2020 at 07:43PM: Under what circumstances is equality of equalities decidable? – stackoverflow.com
StackExchange Bot (Jun 27 2020 at 21:48):Max Heiber posted a new question on June 27, 2020 at 11:22PM: How can I rename an existentially quantified variable in a hypothesis? – stackoverflow.com
StackExchange Bot (Jun 28 2020 at 10:48):Sven Williamson posted a new question on June 28, 2020 at 12:30PM: Weak Excluded Middle Implies Morgan law for conjunction – stackoverflow.com
StackExchange Bot (Jun 28 2020 at 21:48):Frank Bryce posted a new question on June 28, 2020 at 04:19AM: Has reinforcement learning been used to prove mathematical theorems? – ai.stackexchange.com
StackExchange Bot (Jun 28 2020 at 22:48):push33n posted a new question on June 28, 2020 at 11:54PM: no error with assert (goal) but error with cut (goal) – stackoverflow.com
StackExchange Bot (Jun 29 2020 at 18:48):Carl Patenaude Poulin posted a new question on June 29, 2020 at 07:52PM: Configure OPAM switch for installation of Coq packages – stackoverflow.com
StackExchange Bot (Jun 30 2020 at 23:48):Mohammad-Ali A'RÂBI posted a new question on July 01, 2020 at 01:43AM: Cyclic type definition in Coq – stackoverflow.com
StackExchange Bot (Jul 01 2020 at 10:48):Jan Tušil posted a new question on July 01, 2020 at 11:50AM: How to communicate to Coq that certain types are equal? – stackoverflow.com
StackExchange Bot (Jul 01 2020 at 23:48):sdpoll posted a new question on July 02, 2020 at 12:54AM: How to get the type of a subterm when you're building a match – stackoverflow.com
StackExchange Bot (Jul 03 2020 at 05:48):TomR posted a new question on July 03, 2020 at 07:32AM: How to model/formalize the change of the variable (change of world) in Isabelle/HOL? – stackoverflow.com
StackExchange Bot (Jul 05 2020 at 10:48):ZhangLiao posted a new question on July 05, 2020 at 12:02PM: Arguments in tactics – stackoverflow.com
StackExchange Bot (Jul 05 2020 at 17:48):rosi javi posted a new question on July 05, 2020 at 07:26PM: How to prove statement is wrong – stackoverflow.com
StackExchange Bot (Jul 07 2020 at 16:48):rosi javi posted a new question on July 07, 2020 at 06:08PM: How to find difference between two statements – stackoverflow.com
StackExchange Bot (Jul 08 2020 at 19:48):rosi javi posted a new question on July 07, 2020 at 06:08PM: How to provide proof that two values are different? – stackoverflow.com
StackExchange Bot (Jul 09 2020 at 15:48):Marius Melzer posted a new question on July 09, 2020 at 04:57PM: Apply a lemma to a conjunction branch without splitting in coq – stackoverflow.com
StackExchange Bot (Jul 09 2020 at 20:48):raugfer posted a new question on July 09, 2020 at 10:32PM: Issue on definition expansion from Coq module system – stackoverflow.com
StackExchange Bot (Jul 12 2020 at 17:48):rosi javi posted a new question on July 12, 2020 at 07:31PM: How to arrange elements in the list – stackoverflow.com
StackExchange Bot (Jul 13 2020 at 11:48):A Question Asker posted a new question on July 13, 2020 at 01:29PM: Figuring out proper loop invariant when appending to a linked list with verifiable C – stackoverflow.com
StackExchange Bot (Jul 13 2020 at 16:48):A Question Asker posted a new question on July 13, 2020 at 06:46PM: Is it true that field_compatible (tarray (tptr tcell) 0)=(tptr tcell)? Is this approach to the body_incr correct? – stackoverflow.com
StackExchange Bot (Jul 14 2020 at 02:48):kimitsu posted a new question on July 14, 2020 at 04:18AM: Can't compare strings using Coq standard library – stackoverflow.com
StackExchange Bot (Jul 15 2020 at 01:48):frafle posted a new question on July 15, 2020 at 03:26AM: How can I create tuples in Coq and use them as new dataTypes – stackoverflow.com
StackExchange Bot (Jul 15 2020 at 10:48):A Question Asker posted a new question on July 15, 2020 at 12:13PM: Some help proving coq function terminates – stackoverflow.com
StackExchange Bot (Jul 15 2020 at 11:48):A Question Asker posted a new question on July 15, 2020 at 01:01PM: Dependent pattern match asks for a wildcard instead of proper type – stackoverflow.com
StackExchange Bot (Jul 15 2020 at 15:48):user2183336 posted a new question on July 15, 2020 at 05:42PM: exp function in Coq doesn't appear to terminate – stackoverflow.com
StackExchange Bot (Jul 15 2020 at 17:48):user2183336 posted a new question on July 15, 2020 at 07:09PM: First proof over Reals in Coq – stackoverflow.com
StackExchange Bot (Jul 15 2020 at 19:48):user2183336 posted a new question on July 15, 2020 at 09:04PM: coq field tactic fails to simplify, yeilds "m <> 0%R" – stackoverflow.com
StackExchange Bot (Jul 15 2020 at 21:48):frafle posted a new question on July 15, 2020 at 10:49PM: How to use finite sets represented as lists in attributes of a class in Coq? – stackoverflow.com
StackExchange Bot (Jul 16 2020 at 15:48):user2183336 posted a new question on July 16, 2020 at 05:01PM: Solve for a variable in Coq – stackoverflow.com
StackExchange Bot (Jul 16 2020 at 16:48):user2183336 posted a new question on July 16, 2020 at 06:39PM: Show theorem definition in Coq – stackoverflow.com
StackExchange Bot (Jul 19 2020 at 09:48):Potiron posted a new question on July 19, 2020 at 11:43AM: How to define exp for Church Numerals in coq? – stackoverflow.com
StackExchange Bot (Jul 21 2020 at 15:48):A Question Asker posted a new question on July 21, 2020 at 05:04PM: Some help dealing with inject/unject and vector types – stackoverflow.com
StackExchange Bot (Jul 22 2020 at 05:48):Feryll posted a new question on July 22, 2020 at 06:57AM: Abstraction/typing error resulting from case_eq and rewriting in Coq – stackoverflow.com
StackExchange Bot (Jul 22 2020 at 07:48):rosi javi posted a new question on July 22, 2020 at 08:44AM: How to solve contradiction in Coq – stackoverflow.com
StackExchange Bot (Jul 23 2020 at 10:48):A Question Asker posted a new question on July 23, 2020 at 12:03PM: Improving dependently typed reverse function – stackoverflow.com
StackExchange Bot (Jul 23 2020 at 19:48):NJay posted a new question on July 23, 2020 at 08:56PM: Agda equivalent of destruct <term> eqn:<identifier> – stackoverflow.com
StackExchange Bot (Jul 25 2020 at 05:48):sana sobia posted a new question on July 25, 2020 at 07:07AM: How to apply a specific command – stackoverflow.com
StackExchange Bot (Jul 27 2020 at 08:48):A Question Asker posted a new question on July 27, 2020 at 10:33AM: Is there a way to get eauto to properly invoke econstructor? – stackoverflow.com
StackExchange Bot (Jul 28 2020 at 17:48):joshan beha posted a new question on July 28, 2020 at 07:29PM: How simply a statement of lemma – stackoverflow.com
StackExchange Bot (Jul 28 2020 at 20:48):user4035 posted a new question on July 28, 2020 at 10:13PM: How to apply a lemma to 2 hypothesis – stackoverflow.com
StackExchange Bot (Jul 28 2020 at 22:48):user4035 posted a new question on July 28, 2020 at 11:25PM: Coq: help to formalize an informal proof – stackoverflow.com
StackExchange Bot (Jul 29 2020 at 12:48):KöniglichePM posted a new question on July 29, 2020 at 02:23PM: How to get the name of a named goal in the coq api – stackoverflow.com
StackExchange Bot (Jul 30 2020 at 12:48):larsr posted a new question on July 30, 2020 at 01:58PM: Using Notations in Records – stackoverflow.com
StackExchange Bot (Jul 30 2020 at 16:48):user4035 posted a new question on July 30, 2020 at 06:31PM: IndProp: prove that Prop is not provable – stackoverflow.com
StackExchange Bot (Jul 31 2020 at 21:48):user8845853 posted a new question on July 31, 2020 at 11:34PM: How to instantiate hypotheses with variables that are out of scope – stackoverflow.com
StackExchange Bot (Jul 31 2020 at 22:48):Laila Elbeheiry posted a new question on August 01, 2020 at 12:29AM: Applying hypothesis with unknown variables – cstheory.stackexchange.com
StackExchange Bot (Aug 01 2020 at 21:48):Max Heiber posted a new question on August 01, 2020 at 10:55PM: Does using the unfold tactic followed by fold in Coq do anything? – stackoverflow.com
StackExchange Bot (Aug 04 2020 at 06:48):user5876164 posted a new question on August 04, 2020 at 08:29AM: How to get cardinal of ensembles explicitly – stackoverflow.com
StackExchange Bot (Aug 05 2020 at 16:48):joshan beha posted a new question on August 05, 2020 at 06:43PM: Greatest value in natural number list – stackoverflow.com
StackExchange Bot (Aug 06 2020 at 21:48):user4035 posted a new question on August 06, 2020 at 11:11PM: Instance of Ord typeclass for option – stackoverflow.com
StackExchange Bot (Aug 07 2020 at 01:48):HTNW posted a new question on August 07, 2020 at 03:41AM: How to prove all proofs of le equal? – stackoverflow.com
StackExchange Bot (Aug 08 2020 at 13:48):Max Heiber posted a new question on August 08, 2020 at 03:15PM: Would giving up on 'ex falso' change anything w.r.t. dependently-typed programming in Coq? – stackoverflow.com
StackExchange Bot (Aug 09 2020 at 09:48):Daisuke posted a new question on August 09, 2020 at 11:28AM: I have trouble on defining Category whose arrows are parametrised functions with Coq – stackoverflow.com
StackExchange Bot (Aug 09 2020 at 10:48):Lemming posted a new question on August 09, 2020 at 12:10PM: ring tactic on Z fails to simplify in exponent – stackoverflow.com
StackExchange Bot (Aug 09 2020 at 12:48):Daisuke posted a new question on August 09, 2020 at 11:28AM: define Category in which arrows are parametrised functions with Coq – stackoverflow.com
StackExchange Bot (Aug 09 2020 at 12:48):wt.cc posted a new question on August 09, 2020 at 02:35PM: What's the exact rule of applying a theorem in Coq? – stackoverflow.com
StackExchange Bot (Aug 09 2020 at 23:48):Daisuke posted a new question on August 09, 2020 at 11:28AM: define Category in which arrows are parametrised functions using Coq – stackoverflow.com
StackExchange Bot (Aug 10 2020 at 15:48):Francesca Pratali posted a new question on August 10, 2020 at 05:16PM: Coq for HoTT: proving || P-> X || -> (P-> ||X||) – stackoverflow.com
StackExchange Bot (Aug 12 2020 at 10:48):Rodrigo posted a new question on August 12, 2020 at 11:56AM: Proving technology of Coq's kernel – stackoverflow.com
StackExchange Bot (Aug 12 2020 at 17:48):push33n posted a new question on August 12, 2020 at 07:07PM: can coq intros pattern split at the rightmost opportunity for conjunction? – stackoverflow.com
StackExchange Bot (Aug 12 2020 at 20:48):user4035 posted a new question on August 12, 2020 at 10:18PM: Coq: unary to binary convertion – stackoverflow.com
StackExchange Bot (Aug 13 2020 at 09:48):Rodrigo posted a new question on August 13, 2020 at 11:29AM: Difference between the logic and the type system of a proof assistant? – cs.stackexchange.com
StackExchange Bot (Aug 14 2020 at 02:48):Pedro Abreu posted a new question on August 14, 2020 at 04:19AM: Avoid implicit arguments of Fixpoint from becoming explicit in proof mode – stackoverflow.com
StackExchange Bot (Aug 14 2020 at 18:48):Artem Kokorin posted a new question on August 14, 2020 at 08:04PM: What are the rules of Coq implicit types deduction in Inductive definitions? – stackoverflow.com
StackExchange Bot (Aug 14 2020 at 20:48):push33n posted a new question on August 14, 2020 at 09:59PM: string comparison in ssreflect – stackoverflow.com
StackExchange Bot (Aug 15 2020 at 16:48):joshan beha posted a new question on August 15, 2020 at 06:21PM: How to close false statement of lemma – stackoverflow.com
StackExchange Bot (Aug 15 2020 at 19:48):push33n posted a new question on August 15, 2020 at 09:13PM: cannot rename things with dependent induction? – stackoverflow.com
StackExchange Bot (Aug 21 2020 at 13:52):Abe posted a new question on August 21, 2020 at 03:35PM: Not explicitly specifying instances of a type in coq – stackoverflow.com
StackExchange Bot (Aug 22 2020 at 18:48):joshan beha posted a new question on August 22, 2020 at 08:24PM: How to make constraints simple – stackoverflow.com
StackExchange Bot (Aug 23 2020 at 17:48):joshan beha posted a new question on August 23, 2020 at 07:23PM: Inversion tactics in coq – stackoverflow.com
StackExchange Bot (Aug 24 2020 at 10:48):Rodrigo posted a new question on August 24, 2020 at 12:19PM: What are the differences in the encoding of logics in Isabelle and Coq? – stackoverflow.com
StackExchange Bot (Aug 24 2020 at 11:48):Rodrigo posted a new question on August 24, 2020 at 12:19PM: How are logics encoded in Coq? – stackoverflow.com
StackExchange Bot (Aug 26 2020 at 15:48):Kaind posted a new question on August 26, 2020 at 04:52PM: "at next level" in Coq? – stackoverflow.com
StackExchange Bot (Aug 27 2020 at 18:48):Kaind posted a new question on August 27, 2020 at 08:01PM: Proof mode definitions in Coq? – stackoverflow.com
StackExchange Bot (Aug 28 2020 at 14:48):Tilman Zuckmantel posted a new question on August 28, 2020 at 04:18PM: Lemma about Sortedness of concatenated lists – stackoverflow.com
StackExchange Bot (Aug 29 2020 at 18:48):Kaind posted a new question on August 29, 2020 at 08:21PM: Reorder display of hypothesis in Coq? – stackoverflow.com
StackExchange Bot (Aug 31 2020 at 12:48):Sven Williamson posted a new question on August 31, 2020 at 02:00PM: Issue around the 'elim restriction' – stackoverflow.com
StackExchange Bot (Sep 01 2020 at 10:48):Rodrigo posted a new question on August 30, 2020 at 05:59PM: Does lean enhance proof surveyability? – stackoverflow.com
StackExchange Bot (Sep 01 2020 at 15:48):Rodrigo posted a new question on September 01, 2020 at 05:22PM: Can HOL be simulated in the CiC? – cs.stackexchange.com
StackExchange Bot (Sep 02 2020 at 15:48):Kaind posted a new question on September 02, 2020 at 04:53PM: Records as Prop? – stackoverflow.com
StackExchange Bot (Sep 02 2020 at 15:48):Kaind posted a new question on September 02, 2020 at 04:57PM: Curry Howard correspondance in Coq – stackoverflow.com
StackExchange Bot (Sep 02 2020 at 16:48):Kaind posted a new question on September 02, 2020 at 04:57PM: Curry Howard correspondence in Coq – stackoverflow.com
StackExchange Bot (Sep 03 2020 at 15:48):Kiran Gopinathan posted a new question on September 03, 2020 at 05:14PM: Verifying programs with heterogeneous arrays in VST – stackoverflow.com
StackExchange Bot (Sep 03 2020 at 17:48):Labbekak posted a new question on September 03, 2020 at 07:24PM: Coq: induction principles for void, unit and bool from nat and fin – stackoverflow.com
StackExchange Bot (Sep 07 2020 at 09:48):Daisuke Sugawara posted a new question on September 07, 2020 at 11:11AM: trivial theorem about my inductive type on Coq – stackoverflow.com
StackExchange Bot (Sep 08 2020 at 06:48):Daisuke Sugawara posted a new question on September 08, 2020 at 07:43AM: Differential calculus on Coq – stackoverflow.com
StackExchange Bot (Sep 08 2020 at 16:48):joshan beha posted a new question on September 08, 2020 at 06:39PM: How to write statement formally? – stackoverflow.com
StackExchange Bot (Sep 08 2020 at 23:48):user3712960 posted a new question on September 09, 2020 at 01:17AM: Backward Induction principle – stackoverflow.com
StackExchange Bot (Sep 09 2020 at 04:48):Daisuke Sugawara posted a new question on September 09, 2020 at 06:36AM: Pattern match with two list whose type is dependent type on Coq – stackoverflow.com
StackExchange Bot (Sep 09 2020 at 06:48):Daisuke Sugawara posted a new question on September 09, 2020 at 08:28AM: exact value of the derivative on Coq – stackoverflow.com
StackExchange Bot (Sep 10 2020 at 05:48):Lance Pollard posted a new question on September 10, 2020 at 07:47AM: How do you lookup the definition or implementation of Coq proof tactics? – stackoverflow.com
StackExchange Bot (Sep 10 2020 at 07:48):joshan beha posted a new question on September 10, 2020 at 09:22AM: Equal relation between two terms – stackoverflow.com
StackExchange Bot (Sep 14 2020 at 01:48):Landon D. C. Elkind posted a new question on September 14, 2020 at 03:02AM: Coq: Ltac for transitivity of implication (a.k.a. hypothetical syllogism) – stackoverflow.com
StackExchange Bot (Sep 15 2020 at 09:48):Daisuke Sugawara posted a new question on September 15, 2020 at 11:46AM: Partial derivative with Coquelicot on Coq – stackoverflow.com
StackExchange Bot (Sep 15 2020 at 13:48):Daisuke Sugawara posted a new question on September 15, 2020 at 02:39PM: Partial differentiation using Coqelicot on Coq – stackoverflow.com
StackExchange Bot (Sep 17 2020 at 09:48):Daisuke Sugawara posted a new question on September 17, 2020 at 11:46AM: Last n elements of list whose type is dependent type on Coq – stackoverflow.com
StackExchange Bot (Sep 17 2020 at 17:48):Daniel Hines posted a new question on September 17, 2020 at 06:49PM: Reusing lia tactic to prove decidability – stackoverflow.com
StackExchange Bot (Sep 18 2020 at 12:48):Daisuke Sugawara posted a new question on September 18, 2020 at 02:35PM: Vector error : The type of this term is a product – stackoverflow.com
StackExchange Bot (Sep 19 2020 at 11:48):Daisuke Sugawara posted a new question on September 19, 2020 at 01:41PM: Don't arrow arguments that don't meet conditions – stackoverflow.com
StackExchange Bot (Sep 20 2020 at 02:48):Daisuke Sugawara posted a new question on September 20, 2020 at 04:35AM: Can we ban arguments that don't meet conditions? – stackoverflow.com
StackExchange Bot (Sep 21 2020 at 11:48):Daisuke Sugawara posted a new question on September 21, 2020 at 01:24PM: Guarantee the length of the list on Coq – stackoverflow.com
StackExchange Bot (Sep 21 2020 at 12:48):12412316 posted a new question on September 21, 2020 at 02:03PM: Can I print the partial definition of not finished proof in coq? – stackoverflow.com
StackExchange Bot (Sep 21 2020 at 17:59):Rodrigo posted a new question on September 21, 2020 at 07:51PM: Using a module's definition in Coq – stackoverflow.com
StackExchange Bot (Sep 22 2020 at 13:48):Daisuke Sugawara posted a new question on September 21, 2020 at 01:24PM: Transform the lemma leaving previous state on Coq – stackoverflow.com
StackExchange Bot (Sep 24 2020 at 14:48):Dole posted a new question on September 24, 2020 at 04:04PM: Defining Addition Over Integers in Coq – stackoverflow.com
StackExchange Bot (Sep 26 2020 at 04:48):Sajuuk posted a new question on September 26, 2020 at 06:47AM: Why isn't plus_assoc rewriting correctly? – cs.stackexchange.com
StackExchange Bot (Sep 26 2020 at 17:48):Sajuuk posted a new question on September 26, 2020 at 07:33PM: why is behaviour of simpl differ so much after a commutative operation and how to inspect simpl? – cs.stackexchange.com
StackExchange Bot (Sep 26 2020 at 18:48):Bob posted a new question on September 26, 2020 at 08:35PM: Impredicative Set and axioms – cstheory.stackexchange.com
StackExchange Bot (Sep 29 2020 at 20:48):Dan Johnson posted a new question on September 29, 2020 at 10:18PM: is there any tactic in Coq that can transform a bool expression to a Prop one? – stackoverflow.com
StackExchange Bot (Sep 29 2020 at 20:48):Joonazan posted a new question on September 29, 2020 at 10:23PM: How to index a tuple with ssreflect ordinals – stackoverflow.com
StackExchange Bot (Sep 30 2020 at 11:48):ewokonfire posted a new question on September 30, 2020 at 01:16PM: Coq: How do I prove that forall n m : nat, (n > m) -> (S n > S m)? – stackoverflow.com
StackExchange Bot (Oct 02 2020 at 02:48):Dan Johnson posted a new question on October 02, 2020 at 04:13AM: Coq error: Unable to unify "true" with "is_true (0 < a - b - 3)" – stackoverflow.com
StackExchange Bot (Oct 03 2020 at 15:48):Dan Johnson posted a new question on October 03, 2020 at 05:26PM: Can I use destruct here given the constraint I have for index range of a list? – stackoverflow.com
StackExchange Bot (Oct 05 2020 at 02:48):Dan Johnson posted a new question on October 05, 2020 at 04:13AM: If two constructor expressions of an inductive type are equal in Coq, can I do rewriting based on their corresponding arguments? – stackoverflow.com
StackExchange Bot (Oct 05 2020 at 13:48):Daisuke Sugawara posted a new question on October 05, 2020 at 03:21PM: Append and Split is same as doing nothing – stackoverflow.com
StackExchange Bot (Oct 05 2020 at 16:48):Finn posted a new question on October 05, 2020 at 06:24PM: How can I prevent Coq notations in closed scopes interfering with notations in open ones? – stackoverflow.com
StackExchange Bot (Oct 06 2020 at 07:48):Morin posted a new question on October 06, 2020 at 09:26AM: Is there a tactic to help resolving existential qualifiers in Coq? – cs.stackexchange.com
StackExchange Bot (Oct 06 2020 at 07:48):Spielzeug posted a new question on October 06, 2020 at 09:40AM: Equality function in Coq – stackoverflow.com
StackExchange Bot (Oct 06 2020 at 11:48):Morin posted a new question on October 06, 2020 at 09:26AM: Is there a tactic to help resolving existential quantifiers in Coq? – cs.stackexchange.com
StackExchange Bot (Oct 06 2020 at 12:51):Daisuke Sugawara posted a new question on October 06, 2020 at 02:17PM: Vector : t A n = t A (n+0)? – stackoverflow.com
StackExchange Bot (Oct 06 2020 at 21:48):Dan Johnson posted a new question on October 06, 2020 at 11:37PM: Take a conjunction of two hypotheses and create a new hypothesis in Coq – stackoverflow.com
StackExchange Bot (Oct 07 2020 at 03:48):Dan Johnson posted a new question on October 07, 2020 at 05:34AM: How can I build a list of bytes from its specification in Coq – stackoverflow.com
StackExchange Bot (Oct 07 2020 at 08:48):Daisuke Sugawara posted a new question on October 07, 2020 at 09:51AM: Vector: split a vector with n which is the same as vector's length – stackoverflow.com
StackExchange Bot (Oct 07 2020 at 09:48):Daisuke Sugawara posted a new question on October 07, 2020 at 09:51AM: Vector: theorem about splitting and appending vectors – stackoverflow.com
StackExchange Bot (Oct 07 2020 at 14:51):jvrn3 posted a new question on October 07, 2020 at 04:47PM: What does Proof. simpl. reflexivity. Qed. mean in Coq? – stackoverflow.com
StackExchange Bot (Oct 08 2020 at 14:48):Daisuke Sugawara posted a new question on October 08, 2020 at 04:24PM: Teach Coq that associative law of natural numbers holds – stackoverflow.com
StackExchange Bot (Oct 09 2020 at 00:48):nd2 posted a new question on October 09, 2020 at 02:46AM: normalize (normalize n) = normalize (n) – stackoverflow.com
StackExchange Bot (Oct 09 2020 at 13:48):Daisuke Sugawara posted a new question on October 09, 2020 at 02:51PM: Vector: take out some elements from a vector with two methods – stackoverflow.com
StackExchange Bot (Oct 10 2020 at 07:48):user4035 posted a new question on October 10, 2020 at 09:26AM: Quick Chick eqBoolArrowA_correct theorem – stackoverflow.com
StackExchange Bot (Oct 10 2020 at 20:48):user4035 posted a new question on October 10, 2020 at 10:40PM: Coq Z_3 group definition left id theorem – stackoverflow.com
StackExchange Bot (Oct 11 2020 at 08:48):Daisuke Sugawara posted a new question on October 11, 2020 at 10:41AM: Prove equality of lists with list_beq – stackoverflow.com
StackExchange Bot (Oct 11 2020 at 11:48):Daisuke Sugawara posted a new question on October 11, 2020 at 01:43PM: Equality on type which is not inductive type – stackoverflow.com
StackExchange Bot (Oct 11 2020 at 15:48):mia_h posted a new question on October 11, 2020 at 04:03PM: How to prove that the subsequence of an empty list is empty? – stackoverflow.com
StackExchange Bot (Oct 12 2020 at 06:48):Daisuke Sugawara posted a new question on October 12, 2020 at 07:59AM: A list transformed from a vector equals to a list transformed from a vector casted its type – stackoverflow.com
StackExchange Bot (Oct 15 2020 at 03:48):Sajuuk posted a new question on October 15, 2020 at 04:47AM: Why discriminate the base case allows me to complete the induction proof? – cs.stackexchange.com
StackExchange Bot (Oct 15 2020 at 08:48):user4035 posted a new question on October 15, 2020 at 10:24AM: Proof irrelevance for boolean equality – stackoverflow.com
StackExchange Bot (Oct 15 2020 at 15:48):user4035 posted a new question on October 15, 2020 at 04:54PM: Z_3: left id proof – stackoverflow.com
StackExchange Bot (Oct 16 2020 at 06:48):TexasRattleSnake posted a new question on October 16, 2020 at 08:25AM: Inductive proposition for sublists in Coq – stackoverflow.com
StackExchange Bot (Oct 16 2020 at 21:48):mia_h posted a new question on October 16, 2020 at 11:45PM: How to apply a constructor in an hypothesis? – stackoverflow.com
StackExchange Bot (Oct 16 2020 at 22:48):user4035 posted a new question on October 17, 2020 at 12:35AM: Z_3: left inversion lemma. How to add 1 + 1 + 1 – stackoverflow.com
StackExchange Bot (Oct 17 2020 at 21:48):gust posted a new question on October 17, 2020 at 11:22PM: Coq unable to unify -- how to change hypothesis? – stackoverflow.com
StackExchange Bot (Oct 18 2020 at 09:48):user4035 posted a new question on October 17, 2020 at 12:35AM: Z_3: left inversion lemma – stackoverflow.com
StackExchange Bot (Oct 18 2020 at 15:48):Lessness Randomness posted a new question on October 18, 2020 at 05:08PM: How to prove equivalence between those two types - algorithm' and algorithm''? – stackoverflow.com
StackExchange Bot (Oct 21 2020 at 14:48):Daisuke Sugawara posted a new question on October 21, 2020 at 04:25PM: Equality on complex functions – stackoverflow.com
StackExchange Bot (Oct 21 2020 at 15:48):Lessness Randomness posted a new question on October 21, 2020 at 05:40PM: Is there a good strategy for proving the given teorem? – stackoverflow.com
StackExchange Bot (Oct 22 2020 at 12:48):Daisuke Sugawara posted a new question on October 22, 2020 at 02:08PM: Equality on complex functions part 2 – stackoverflow.com
StackExchange Bot (Oct 23 2020 at 11:48):Daisuke Sugawara posted a new question on October 22, 2020 at 02:08PM: Equality on complex functions with complex type – stackoverflow.com
StackExchange Bot (Oct 24 2020 at 03:48):sxysun posted a new question on October 24, 2020 at 05:46AM: Automatically proving a non-linear arithmetic proposition over Z in Coq – stackoverflow.com
StackExchange Bot (Oct 26 2020 at 11:48):Daisuke Sugawara posted a new question on October 26, 2020 at 12:03PM: Different arguments, but behavior of function is same – stackoverflow.com
StackExchange Bot (Oct 27 2020 at 07:48):kimitsu posted a new question on October 27, 2020 at 08:46AM: Can't bind variable to wrapped open formula – stackoverflow.com
StackExchange Bot (Oct 27 2020 at 22:48):Lessness Randomness posted a new question on October 21, 2020 at 05:40PM: Is there a good strategy for proving the given theorem? – stackoverflow.com
StackExchange Bot (Oct 28 2020 at 17:48):Tejas Shah posted a new question on October 28, 2020 at 05:59PM: How does the grading script of the LF series work for manually graded exercises? – stackoverflow.com
StackExchange Bot (Nov 03 2020 at 17:48):Richard Southwell posted a new question on November 03, 2020 at 06:30PM: Dependent functions in Coq – stackoverflow.com
StackExchange Bot (Nov 03 2020 at 22:48):Richard Southwell posted a new question on November 03, 2020 at 11:19PM: Functions from empty set in Coq – stackoverflow.com
StackExchange Bot (Nov 04 2020 at 08:48):Baber posted a new question on November 04, 2020 at 09:31AM: Can we define recursive definitions in Coq? – stackoverflow.com
StackExchange Bot (Nov 04 2020 at 23:49):Yarick posted a new question on November 05, 2020 at 12:31AM: Stuck with a proof – stackoverflow.com
StackExchange Bot (Nov 07 2020 at 19:48):Leo Orshansky posted a new question on November 07, 2020 at 08:44PM: Coq - How can you apply an implication with a match clause? – stackoverflow.com
StackExchange Bot (Nov 08 2020 at 19:48):Taylor Roberts posted a new question on November 08, 2020 at 08:13PM: Predicate Logic in Coq – stackoverflow.com
StackExchange Bot (Nov 09 2020 at 10:48):MayJuneJuly posted a new question on November 09, 2020 at 11:12AM: Predicate Logic in coq: red tactic – stackoverflow.com
StackExchange Bot (Nov 09 2020 at 15:48):MayJuneJuly posted a new question on November 09, 2020 at 11:12AM: Predicate Logic in coq: – stackoverflow.com
StackExchange Bot (Nov 09 2020 at 16:51):user2809176 posted a new question on November 09, 2020 at 04:55PM: Coq destruct with an excluding precondition – stackoverflow.com
StackExchange Bot (Nov 09 2020 at 17:48):MayJuneJuly posted a new question on November 09, 2020 at 06:46PM: Coq syntax. Predicate Logic – stackoverflow.com
StackExchange Bot (Nov 11 2020 at 02:48):blaineh posted a new question on November 11, 2020 at 03:09AM: match goal doesn't match let destructuring expression – stackoverflow.com
StackExchange Bot (Nov 11 2020 at 12:48):Iaroslav Baranov posted a new question on November 11, 2020 at 01:07PM: Has somebody tried to use a proof assistant (coq) to do exercises from Cormen or Knuth? – stackoverflow.com
StackExchange Bot (Nov 11 2020 at 14:48):Miguel N. posted a new question on November 11, 2020 at 03:29PM: Error when defining custom notation for an embedded logic – stackoverflow.com
StackExchange Bot (Nov 12 2020 at 16:48):gust posted a new question on November 12, 2020 at 05:05PM: Make two arbitrary variables the same in Coq – stackoverflow.com
StackExchange Bot (Nov 12 2020 at 21:48):gust posted a new question on November 12, 2020 at 10:13PM: Stuck on Coq proof with list induction – stackoverflow.com
StackExchange Bot (Nov 14 2020 at 15:48):Max Heiber posted a new question on November 14, 2020 at 04:21PM: Coq: Syntax error 'Type' or 'Types' expected after 'Implicit' – stackoverflow.com
StackExchange Bot (Nov 14 2020 at 20:48):Mickelsinver posted a new question on November 14, 2020 at 09:26PM: Handling forall inside an hypothesis – stackoverflow.com
StackExchange Bot (Nov 15 2020 at 06:48):Youhei Okubo posted a new question on November 15, 2020 at 07:27AM: How can I construct terms in first-order logic using Coq? – stackoverflow.com
StackExchange Bot (Nov 15 2020 at 11:48):Daisuke Sugawara posted a new question on November 15, 2020 at 11:52AM: Prove equation involving partial derivative analytically with Coq – stackoverflow.com
StackExchange Bot (Nov 17 2020 at 02:48):Daisuke Sugawara posted a new question on November 17, 2020 at 03:30AM: diffefentiation of (1/2)*(x-y)^2 on x is x - y – stackoverflow.com
StackExchange Bot (Nov 17 2020 at 07:48):Daisuke Sugawara posted a new question on November 17, 2020 at 08:43AM: Difinition of equality among vectors – stackoverflow.com
StackExchange Bot (Nov 17 2020 at 13:48):Daisuke Sugawara posted a new question on November 17, 2020 at 08:43AM: Definition of equality among vectors – stackoverflow.com
StackExchange Bot (Nov 19 2020 at 00:48):Mickelsinver posted a new question on November 19, 2020 at 12:58AM: Can I avoid using Option A when I know that head cannot fail? – stackoverflow.com
StackExchange Bot (Nov 19 2020 at 14:48):Daisuke Sugawara posted a new question on November 19, 2020 at 03:08PM: Trivial lemma on real numbers on Coq – stackoverflow.com
StackExchange Bot (Nov 20 2020 at 11:48):Daisuke Sugawara posted a new question on November 20, 2020 at 12:33PM: Theorem about vectors and recursive functions – stackoverflow.com
StackExchange Bot (Nov 20 2020 at 14:48):Jacob Keunen posted a new question on November 20, 2020 at 01:49PM: Induction with other base case in Coq – stackoverflow.com
StackExchange Bot (Nov 21 2020 at 13:48):manfey posted a new question on November 21, 2020 at 02:22PM: Translating coq statment to 'math' – mathoverflow.net
StackExchange Bot (Nov 22 2020 at 15:48):user2809176 posted a new question on November 22, 2020 at 04:02PM: Coq prove a false list assumption – stackoverflow.com
StackExchange Bot (Nov 23 2020 at 11:48):Daisuke Sugawara posted a new question on November 23, 2020 at 12:29PM: split tail of the vector and append head of same vector – stackoverflow.com
StackExchange Bot (Nov 26 2020 at 10:48):Pierre Jouvelot posted a new question on November 26, 2020 at 11:28AM: Type coercion from nat to rat – stackoverflow.com
StackExchange Bot (Nov 27 2020 at 00:48):Nikita Mescheryackov posted a new question on November 27, 2020 at 12:20AM: Proofs of simple arithmetic expressions – stackoverflow.com
StackExchange Bot (Nov 27 2020 at 19:48):Jan Tušil posted a new question on November 27, 2020 at 08:03PM: Unable to satisfy the following constraints: In environment – stackoverflow.com
StackExchange Bot (Nov 30 2020 at 21:48):Alex Coleman posted a new question on November 30, 2020 at 10:44PM: Unable to find Coq library: Error: Unable to locate library Floats. – stackoverflow.com
StackExchange Bot (Dec 01 2020 at 09:48):Daisuke Sugawara posted a new question on December 01, 2020 at 08:57AM: Differentiate inner product on a element of a vector – stackoverflow.com
StackExchange Bot (Dec 02 2020 at 16:48):Tony Peterson posted a new question on December 02, 2020 at 05:04PM: Why are all numeric literals in Coq showing nat type? – stackoverflow.com
StackExchange Bot (Dec 03 2020 at 06:48):gust posted a new question on December 03, 2020 at 07:07AM: coqc -Qreturns "coqc: -Q: no such file or directory" – stackoverflow.com
StackExchange Bot (Dec 03 2020 at 09:48):Daisuke Sugawara posted a new question on December 03, 2020 at 10:27AM: Match the original value of the pattern match with branch value – stackoverflow.com
StackExchange Bot (Dec 03 2020 at 21:48):ZhangLiao posted a new question on December 03, 2020 at 09:06PM: How could we specify the times of running a tactic – stackoverflow.com
StackExchange Bot (Dec 04 2020 at 05:48):Daisuke Sugawara posted a new question on December 04, 2020 at 06:32AM: Differentiate the function id on an element of vector – stackoverflow.com
StackExchange Bot (Dec 04 2020 at 14:48):mia_h posted a new question on December 04, 2020 at 02:49PM: Arithmetic expressions and big-step semantic – stackoverflow.com
StackExchange Bot (Dec 04 2020 at 20:48):Mark posted a new question on December 04, 2020 at 09:11PM: Modeling Cardinality of Finite Sets in Coq – stackoverflow.com
StackExchange Bot (Dec 06 2020 at 07:48):R2D2 posted a new question on December 06, 2020 at 08:14AM: How do I write a proof for a switch statement with VST/ coq? – stackoverflow.com
StackExchange Bot (Dec 06 2020 at 16:48):Sven Williamson posted a new question on December 06, 2020 at 04:48PM: Existence of a bijection between nat and nat * nat in Coq – stackoverflow.com
StackExchange Bot (Dec 07 2020 at 11:48):Daisuke Sugawara posted a new question on December 07, 2020 at 12:34PM: VecUtil: take nth element of processed vector by two slightly different way – stackoverflow.com
StackExchange Bot (Dec 10 2020 at 16:48):kimitsu posted a new question on December 10, 2020 at 05:33PM: How to prove forall x : R, 0 < x -> 0 < x / 2 < x? – stackoverflow.com
StackExchange Bot (Dec 11 2020 at 11:48):Max Heiber posted a new question on December 11, 2020 at 11:51AM: Is the only difference between Inductive and CoInductive the well-formedness checks on their uses (in Coq)? – stackoverflow.com
StackExchange Bot (Dec 11 2020 at 11:48):Max Heiber posted a new question on December 11, 2020 at 12:19PM: Is it possible to define a tactic that unfolds a cofix by one step in Coq? – stackoverflow.com
StackExchange Bot (Dec 11 2020 at 17:48):joshan beha posted a new question on December 11, 2020 at 06:10PM: less than relation between two natural numbers – stackoverflow.com
StackExchange Bot (Dec 13 2020 at 13:48):Blueper posted a new question on December 13, 2020 at 02:25PM: is there a tactic (other than inversion) that extracts implications from hypotheses? – stackoverflow.com
StackExchange Bot (Dec 15 2020 at 20:48):Warrick Macmillan posted a new question on December 15, 2020 at 09:44PM: Record Subtyping in Coq, questions and references requested – stackoverflow.com
StackExchange Bot (Dec 17 2020 at 16:48):geeky90846 posted a new question on December 17, 2020 at 05:10PM: Simulation of global and local variables in Coq – stackoverflow.com
StackExchange Bot (Dec 19 2020 at 04:48):blaineh posted a new question on December 19, 2020 at 04:48AM: Induction order for relation between three lists – stackoverflow.com
StackExchange Bot (Dec 19 2020 at 04:48):Gregory posted a new question on December 19, 2020 at 05:17AM: Fine-grained builds with dynamic dependencies? – stackoverflow.com
StackExchange Bot (Dec 21 2020 at 14:48):Alex Coleman posted a new question on December 21, 2020 at 02:56PM: While it is expected to have type "forall..." in Coq – stackoverflow.com
StackExchange Bot (Dec 21 2020 at 16:48):joshan beha posted a new question on December 21, 2020 at 05:23PM: reduction in the elements of list – stackoverflow.com
StackExchange Bot (Dec 21 2020 at 21:48):Matheus Monteiro posted a new question on December 21, 2020 at 10:07PM: Defining functions inside proof scope – stackoverflow.com
StackExchange Bot (Dec 22 2020 at 17:48):joshan beha posted a new question on December 22, 2020 at 06:46PM: Counting of natural number – stackoverflow.com
StackExchange Bot (Dec 23 2020 at 05:48):Baber posted a new question on December 23, 2020 at 06:05AM: Why Coq doesn't allow a theorem with admits to end with QED in Linux and Windows? – stackoverflow.com
StackExchange Bot (Dec 23 2020 at 17:48):zeesha huq posted a new question on December 23, 2020 at 06:30PM: Effect of non zero term – stackoverflow.com
StackExchange Bot (Dec 24 2020 at 19:48):Hugo Carvalho de Paula posted a new question on December 24, 2020 at 07:45PM: What is the name of the programming style enabled by dependent types (think Coq or Agda)? – stackoverflow.com
StackExchange Bot (Dec 25 2020 at 06:48):joshan beha posted a new question on December 25, 2020 at 07:42AM: Conversion of a statement in formal language – stackoverflow.com
StackExchange Bot (Dec 28 2020 at 08:48):zeesha huq posted a new question on December 28, 2020 at 08:53AM: Less than relationship of natural numbers – stackoverflow.com
StackExchange Bot (Dec 29 2020 at 15:48):Henry Story posted a new question on December 29, 2020 at 03:24PM: Why do Calculus of Construction based languages use Setoids so much? – stackoverflow.com
StackExchange Bot (Dec 29 2020 at 17:48):John Smith posted a new question on December 29, 2020 at 06:10PM: How to pattern match exist to transform proofs – stackoverflow.com
StackExchange Bot (Dec 30 2020 at 03:48):blaineh posted a new question on December 30, 2020 at 04:14AM: How to debug tactic failure in a match goal branch? – stackoverflow.com
StackExchange Bot (Dec 30 2020 at 13:48):Hexirp posted a new question on December 30, 2020 at 02:22PM: How to print 'forall' as 'Π' in a one-time setting in coqdoc? – stackoverflow.com
StackExchange Bot (Dec 30 2020 at 16:48):joshan beha posted a new question on December 30, 2020 at 05:35PM: Finding a function from Library – stackoverflow.com
StackExchange Bot (Jan 06 2021 at 00:48):Isaac van Bakel posted a new question on January 06, 2021 at 01:03AM: How can I generalise Coq proofs of an iff? – stackoverflow.com
StackExchange Bot (Jan 06 2021 at 13:48):Hexirp posted a new question on January 06, 2021 at 02:14PM: Are we sure the Calculus of Inductive Constructions and ZFC plus countably many inaccessible cardinals are equiconsistent? – mathoverflow.net
StackExchange Bot (Jan 06 2021 at 16:48):joshan beha posted a new question on January 06, 2021 at 04:54PM: How to simplify counting relation between natural numbers – stackoverflow.com
StackExchange Bot (Jan 07 2021 at 18:48):Mahnoor dil posted a new question on January 07, 2021 at 06:52PM: prove a lemma sum of all elements of a list l is equal to n, (sortascend n) is equal to n – stackoverflow.com
StackExchange Bot (Jan 08 2021 at 17:48):joshan beha posted a new question on January 08, 2021 at 05:51PM: How to compare two elements of list – stackoverflow.com
StackExchange Bot (Jan 09 2021 at 00:48):Radu Deleanu posted a new question on January 09, 2021 at 01:42AM: Programming c-like classes to run in Coq – stackoverflow.com
StackExchange Bot (Jan 10 2021 at 23:48):Radu Deleanu posted a new question on January 11, 2021 at 12:42AM: list constructors conflict in Coq – stackoverflow.com
StackExchange Bot (Jan 14 2021 at 04:48):Wen Hui Fan posted a new question on January 14, 2021 at 05:23AM: Coq projects cannot be saved properly. Empty file – stackoverflow.com
StackExchange Bot (Jan 14 2021 at 15:48):Schluesselwolf posted a new question on January 14, 2021 at 04:22PM: Coq Newbie: How to iterate trough binary-tree in Coq – stackoverflow.com
StackExchange Bot (Jan 16 2021 at 06:48):juniorxx posted a new question on January 16, 2021 at 07:46AM: How to specialize nested hypotheses in Coq? – stackoverflow.com
StackExchange Bot (Jan 16 2021 at 21:48):Pierre Jouvelot posted a new question on January 16, 2021 at 10:29PM: Problems installing mathcomp 8.12/8.13 via nix on Catalina – stackoverflow.com
StackExchange Bot (Jan 17 2021 at 16:48):juniorxx posted a new question on January 17, 2021 at 04:54PM: How to formalize forall and exists in PLT Redex? – stackoverflow.com
StackExchange Bot (Jan 19 2021 at 05:48):user3565552 posted a new question on January 19, 2021 at 05:49AM: What are the differences between LCF's Theorem and Automath's Prop? – cs.stackexchange.com
StackExchange Bot (Jan 20 2021 at 02:48):user3565552 posted a new question on January 20, 2021 at 03:06AM: How do program types such as natural numbers figure into the Curry-Howard Isomorphism? – cs.stackexchange.com
StackExchange Bot (Jan 20 2021 at 03:48):push33n posted a new question on January 20, 2021 at 03:59AM: can i stack implicit types somehow? – stackoverflow.com
StackExchange Bot (Jan 20 2021 at 04:48):Not me posted a new question on January 20, 2021 at 05:45AM: How is an infinite type hierarchy implemented? – stackoverflow.com
StackExchange Bot (Jan 22 2021 at 12:48):ged posted a new question on January 22, 2021 at 11:57AM: Theorem that finding in a list works properly – stackoverflow.com
StackExchange Bot (Jan 23 2021 at 08:48):tts posted a new question on January 23, 2021 at 08:41AM: What do we call a type system where any term of any type ultimately parses down to $*:\mathbf{1}$? – cstheory.stackexchange.com
StackExchange Bot (Jan 24 2021 at 20:48):Charlie Parker posted a new question on January 24, 2021 at 09:24PM: How does one display the an arbitrary programming language (e.g. Isabelles Isar) in latex in their naive display in pdf? – stackoverflow.com
StackExchange Bot (Jan 26 2021 at 00:48):Charlie Parker posted a new question on January 24, 2021 at 09:24PM: How does one display an arbitrary programming language (e.g. Isabelle/Isar) in latex in their native display in *.pdf format? – stackoverflow.com
StackExchange Bot (Jan 26 2021 at 19:48):user4035 posted a new question on January 26, 2021 at 08:47PM: Error when referencing type variable from another file – stackoverflow.com
StackExchange Bot (Jan 28 2021 at 05:48):Luiz Martins posted a new question on January 28, 2021 at 06:17AM: Printing ssrnat's ".+1" definition – stackoverflow.com
StackExchange Bot (Jan 28 2021 at 20:48):Izzy posted a new question on January 28, 2021 at 09:43PM: What is the meaning of "|-" in coq, and how do I find the definitions for the other seemingly undocumented notations? – stackoverflow.com
StackExchange Bot (Jan 29 2021 at 17:48):NJay posted a new question on January 29, 2021 at 06:43PM: Why can I use the constructor tactic to prove reflexivity? – stackoverflow.com
StackExchange Bot (Jan 31 2021 at 00:48):Luiz Martins posted a new question on January 31, 2021 at 01:10AM: Using the same variable multiple times in a definition to represent equality – stackoverflow.com
StackExchange Bot (Jan 31 2021 at 16:48):Walter Schulze posted a new question on January 31, 2021 at 05:29PM: Rewriting between two equivalent setoids – stackoverflow.com
StackExchange Bot (Feb 02 2021 at 07:48):Hexirp posted a new question on February 02, 2021 at 08:12AM: I know of two ways to define the finite number type. Is there words to distinguish between the two? – stackoverflow.com
StackExchange Bot (Feb 02 2021 at 09:48):Luiz Martins posted a new question on February 02, 2021 at 10:10AM: Introducing a new assumption/hypothesis by adding it as subgoal – stackoverflow.com
StackExchange Bot (Feb 02 2021 at 15:48):Walter Schulze posted a new question on January 31, 2021 at 05:29PM: Coq: Rewriting between two equivalent setoids – stackoverflow.com
StackExchange Bot (Feb 03 2021 at 20:48):Pierre Jouvelot posted a new question on February 03, 2021 at 09:47PM: Lost ".+1" Coq notation in Emacs Proof General Goals buffer – stackoverflow.com
StackExchange Bot (Feb 04 2021 at 09:48):Luiz Martins posted a new question on February 04, 2021 at 10:05AM: Difference between propositionals True/False and booleans true/false in Coq – stackoverflow.com
StackExchange Bot (Feb 04 2021 at 10:48):Quinn Dougherty posted a new question on February 04, 2021 at 10:57AM: Why is preservation not quantified over Gamma? – cstheory.stackexchange.com
StackExchange Bot (Feb 05 2021 at 14:48):fakedrake posted a new question on February 05, 2021 at 03:03PM: Proofs of structural properties of arguments in match in coq – stackoverflow.com
StackExchange Bot (Feb 05 2021 at 20:48):William Oliver posted a new question on February 05, 2021 at 09:33PM: Is it possible to prove forall n: nat, le n 0 -> n = 0. in Coq without using inversion? – stackoverflow.com
StackExchange Bot (Feb 07 2021 at 16:48):user15163266 posted a new question on February 07, 2021 at 05:28PM: how to proof (f1+f1 = f2+f2 -> f1 = f2) in coq – stackoverflow.com
StackExchange Bot (Feb 11 2021 at 07:48):Khan posted a new question on February 11, 2021 at 08:36AM: Reasoning over functions applied to lists of nat in Coq – stackoverflow.com
StackExchange Bot (Feb 11 2021 at 16:48):user7508402 posted a new question on February 11, 2021 at 04:59PM: Coq: parametric rewriting under binders – stackoverflow.com
StackExchange Bot (Feb 12 2021 at 21:48):William Oliver posted a new question on February 12, 2021 at 10:16PM: Removing trivial match clause in Coq – stackoverflow.com
StackExchange Bot (Feb 14 2021 at 10:48):joshan beha posted a new question on February 14, 2021 at 11:19AM: Lemma related to the counting of numbers in list – stackoverflow.com
StackExchange Bot (Feb 16 2021 at 10:48):Jordan Mitchell Barrett posted a new question on February 16, 2021 at 10:56AM: Defining integers inductively in Coq (inductive definitions subject to relations) – stackoverflow.com
StackExchange Bot (Feb 16 2021 at 20:48):Molossus Spondee posted a new question on February 16, 2021 at 08:54PM: Call by name untyped lambda calculus interpreter in Coq – codereview.stackexchange.com
StackExchange Bot (Feb 17 2021 at 14:48):Zhang Liao posted a new question on February 17, 2021 at 03:18PM: Puzzle of induction in Coq – stackoverflow.com
StackExchange Bot (Feb 18 2021 at 14:48):junius posted a new question on February 18, 2021 at 03:28PM: Compiling multiple Coq files does not work – stackoverflow.com
StackExchange Bot (Feb 20 2021 at 14:48):user5876164 posted a new question on February 20, 2021 at 03:34PM: How to prove for all functions P, Q from typical type to Prop, "forall a, b, P(a) or Q(b) holds" iff "forall a, P(a), or, forall b, Q(b), holds"? – stackoverflow.com
StackExchange Bot (Feb 20 2021 at 22:48):Pierre Jouvelot posted a new question on February 20, 2021 at 10:49PM: Translating proof from Nat to Rat – stackoverflow.com
StackExchange Bot (Feb 23 2021 at 07:48):17L251.Swathi.S posted a new question on February 23, 2021 at 08:17AM: How to implement a spec and prove it using kami? – stackoverflow.com
StackExchange Bot (Feb 27 2021 at 17:48):Lance Pollard posted a new question on February 27, 2021 at 06:47PM: How to constrain a type field to a power of two in a type system? – stackoverflow.com
StackExchange Bot (Feb 27 2021 at 23:48):Lance Pollard posted a new question on February 27, 2021 at 11:52PM: How to does "there exists" existential quantifier work in an imperative language? – stackoverflow.com
StackExchange Bot (Feb 28 2021 at 13:48):radrow posted a new question on February 28, 2021 at 01:57PM: Proving coinductive theorems with coinductive assumptions – stackoverflow.com
StackExchange Bot (Mar 01 2021 at 22:48):NJay posted a new question on March 01, 2021 at 10:52PM: Theorem + induction vs Fixpoint + destruct in Coq – stackoverflow.com
StackExchange Bot (Mar 03 2021 at 21:48):Wen Hui Fan posted a new question on March 03, 2021 at 09:47PM: Use coq to define a special Nat Type as below – stackoverflow.com
StackExchange Bot (Mar 04 2021 at 07:48):Wen Hui Fan posted a new question on March 04, 2021 at 07:56AM: Define list length in recursion in Coq Not sure if my function is wrong and got stuck – stackoverflow.com
StackExchange Bot (Mar 04 2021 at 14:48):NJay posted a new question on March 04, 2021 at 03:37PM: Impredicativity + large eliminations (with no excluded middle) in Coq – cstheory.stackexchange.com
StackExchange Bot (Mar 06 2021 at 22:48):domino posted a new question on March 06, 2021 at 11:25PM: Define a polymorphic type in coq – stackoverflow.com
StackExchange Bot (Mar 07 2021 at 01:48):domino posted a new question on March 07, 2021 at 02:39AM: Define polymorphic inductive type tree in coq – stackoverflow.com
StackExchange Bot (Mar 07 2021 at 19:48):domino posted a new question on March 07, 2021 at 08:23PM: Anyone know how mult works in coq? – stackoverflow.com
StackExchange Bot (Mar 11 2021 at 00:48):rexor posted a new question on March 11, 2021 at 12:51AM: Recursive definition of nat_to_bin is ill-formed – stackoverflow.com
StackExchange Bot (Mar 13 2021 at 04:48):zeesha huq posted a new question on March 13, 2021 at 05:34AM: How to write gcd function in Coq – stackoverflow.com
StackExchange Bot (Mar 14 2021 at 23:48):Alex posted a new question on March 15, 2021 at 12:15AM: How to implement a union-find (disjoint set) data structure in Coq? – stackoverflow.com
StackExchange Bot (Mar 15 2021 at 10:48):shooqie posted a new question on March 15, 2021 at 11:40AM: Proving extentional equality of two functions – stackoverflow.com
StackExchange Bot (Mar 15 2021 at 20:48):Reed posted a new question on March 15, 2021 at 09:01PM: I need to derive a .v filetype from a .ott file – stackoverflow.com
StackExchange Bot (Mar 16 2021 at 05:48):Jordan Mitchell Barrett posted a new question on March 16, 2021 at 06:44AM: Coq: evaluating/simplifying Prop tautologies – stackoverflow.com
StackExchange Bot (Mar 16 2021 at 09:48):user1953221 posted a new question on March 16, 2021 at 10:19AM: Case splitting on if-then-else condition – stackoverflow.com
StackExchange Bot (Mar 16 2021 at 21:48):Andrey posted a new question on March 16, 2021 at 09:56PM: Prove commutativity for the sum of two even numbers with dependent types – stackoverflow.com
StackExchange Bot (Mar 17 2021 at 05:48):einzwein posted a new question on March 17, 2021 at 06:07AM: Defining inductive types in intensional type theory purely in terms of type-theoretic data – cstheory.stackexchange.com
StackExchange Bot (Mar 17 2021 at 20:48):Andrey posted a new question on March 16, 2021 at 09:56PM: Postulate and prove theorem about equality for different types (Prove commutativity for the sum of two even numbers with dependent types) – stackoverflow.com
StackExchange Bot (Mar 19 2021 at 14:48):addtip posted a new question on March 19, 2021 at 02:57PM: Coq leb <=? does not give me an hypothesis after case or induction – stackoverflow.com
StackExchange Bot (Mar 19 2021 at 16:48):GhaS Shee posted a new question on March 19, 2021 at 05:33PM: coq-HoTT: How to prove 1 < 2? – stackoverflow.com
StackExchange Bot (Mar 19 2021 at 20:48):addtip posted a new question on March 19, 2021 at 09:26PM: Finding rewrite rules – stackoverflow.com
StackExchange Bot (Mar 20 2021 at 16:48):zeesha huq posted a new question on March 20, 2021 at 05:37PM: How to solve greater or equal relation between two numbers – stackoverflow.com
StackExchange Bot (Mar 22 2021 at 15:48):SD01 posted a new question on March 22, 2021 at 04:38PM: Coq begginer here, how to understand the syntax? – stackoverflow.com
StackExchange Bot (Mar 22 2021 at 21:48):granduser posted a new question on March 22, 2021 at 10:18PM: Coq proving nonsensical inductive property implication? – stackoverflow.com
StackExchange Bot (Mar 26 2021 at 07:48):Andrew W posted a new question on March 26, 2021 at 08:15AM: In Coq, is there a way to see the tactics applied by tauto? – stackoverflow.com
StackExchange Bot (Mar 26 2021 at 13:48):zeesha huq posted a new question on March 26, 2021 at 02:31PM: Use of contradiction statement – stackoverflow.com
StackExchange Bot (Mar 27 2021 at 00:48):Jordan Mitchell Barrett posted a new question on March 27, 2021 at 01:40AM: Coq - function choosing witnesses for a forall-exists statement – stackoverflow.com
StackExchange Bot (Mar 28 2021 at 05:48):Jordan Mitchell Barrett posted a new question on March 28, 2021 at 07:00AM: Coq - adding choice function to context – stackoverflow.com
StackExchange Bot (Mar 28 2021 at 10:48):einzwein posted a new question on March 28, 2021 at 12:26PM: Dependent eliminator for empty type in intensional Martin-Löf type theory – cstheory.stackexchange.com
StackExchange Bot (Mar 28 2021 at 13:53):Shubham Sondhi posted a new question on March 28, 2021 at 03:44PM: How to deal with "false = true" proposition while proving theorems in coq – stackoverflow.com
StackExchange Bot (Mar 28 2021 at 22:48):LeBaguette posted a new question on March 29, 2021 at 12:22AM: How do I prove false from a false hypothesis? – stackoverflow.com
StackExchange Bot (Mar 29 2021 at 16:48):R. Bosman posted a new question on March 29, 2021 at 06:13PM: How do I exclude a certain form in a hint for autorewrite? – stackoverflow.com
StackExchange Bot (Mar 30 2021 at 00:48):D. Ben Knoble posted a new question on March 30, 2021 at 02:14AM: Unfold a type-function in a match (like destruct) – stackoverflow.com
StackExchange Bot (Mar 30 2021 at 08:48):R. Bosman posted a new question on March 29, 2021 at 06:13PM: Add ltac expression as hint to autorewrite? – stackoverflow.com
StackExchange Bot (Mar 30 2021 at 09:48):user65526 posted a new question on March 30, 2021 at 10:52AM: Pairs and projections in Coq – stackoverflow.com
StackExchange Bot (Mar 31 2021 at 03:48):Jordan Mitchell Barrett posted a new question on March 31, 2021 at 05:31AM: Coq can't infer type parameter in match – stackoverflow.com
StackExchange Bot (Mar 31 2021 at 08:48):Philémon Berstel-Da Silva posted a new question on March 31, 2021 at 10:38AM: How to prove the decomposition of implication? – stackoverflow.com
StackExchange Bot (Apr 01 2021 at 02:48):domino posted a new question on April 01, 2021 at 04:45AM: define edges for undirected graph in coq – stackoverflow.com
StackExchange Bot (Apr 01 2021 at 23:48):Shubham Sondhi posted a new question on April 02, 2021 at 01:13AM: Coq proof stuck in a loop – stackoverflow.com
StackExchange Bot (Apr 02 2021 at 08:48):Shubham Sondhi posted a new question on April 02, 2021 at 10:14AM: Loop while proving a theorem – stackoverflow.com
StackExchange Bot (Apr 02 2021 at 22:48):Marco Servetto posted a new question on April 03, 2021 at 12:21AM: Coq Notation Syntax error: [term level 200] expected after [term level 200] (in [term]) – stackoverflow.com
StackExchange Bot (Apr 03 2021 at 13:48):steve01 posted a new question on April 03, 2021 at 03:22PM: What tactic should I use to avoid stucking in endless loop, in Coq? – stackoverflow.com
StackExchange Bot (Apr 04 2021 at 22:48):rausted posted a new question on April 05, 2021 at 12:46AM: Coq Vector explode in proof mode? – stackoverflow.com
StackExchange Bot (Apr 06 2021 at 11:48):ieja posted a new question on April 06, 2021 at 12:58PM: Mix-up of bool and Datatypes.bool after Require Import coq libraries – stackoverflow.com
StackExchange Bot (Apr 07 2021 at 10:48):ieja posted a new question on April 07, 2021 at 11:48AM: Coq infotheo %B is_true – stackoverflow.com
StackExchange Bot (Apr 08 2021 at 03:48):domino posted a new question on April 08, 2021 at 05:27AM: How to prove one nat is less than or equal to another nat in coq? – stackoverflow.com
StackExchange Bot (Apr 08 2021 at 07:48):domino posted a new question on April 08, 2021 at 09:28AM: How to prove n <= n + S m in coq? – stackoverflow.com
StackExchange Bot (Apr 08 2021 at 16:49):D. Ben Knoble posted a new question on April 08, 2021 at 06:24PM: Dependent-type design when the parameters indicate the result should not exist – stackoverflow.com
StackExchange Bot (Apr 08 2021 at 17:48):Marco Mantovani posted a new question on April 08, 2021 at 07:01PM: FoldR using FoldL on finite lists – stackoverflow.com
StackExchange Bot (Apr 08 2021 at 18:48):Jan Tušil posted a new question on April 08, 2021 at 07:55PM: Tower of powersets – stackoverflow.com
StackExchange Bot (Apr 09 2021 at 07:48):ieja posted a new question on April 09, 2021 at 09:26AM: Coq infotheo Unable to Unify error when comparing sums of reals – stackoverflow.com
StackExchange Bot (Apr 09 2021 at 11:48):Veky posted a new question on April 09, 2021 at 01:41PM: coq auto says simple apply fails but it works manually – stackoverflow.com
StackExchange Bot (Apr 10 2021 at 10:48):ieja posted a new question on April 10, 2021 at 12:01PM: Cauchy-Schwartz Inequality in Coq? – stackoverflow.com
StackExchange Bot (Apr 10 2021 at 12:48):user15598472 posted a new question on April 10, 2021 at 02:31PM: "Symbol's value as variable is void" when adding a path to coqtop when opening emacs – stackoverflow.com
StackExchange Bot (Apr 13 2021 at 05:48):domino posted a new question on April 13, 2021 at 07:04AM: Implement Boruvka's algorithm in Coq – stackoverflow.com
StackExchange Bot (Apr 14 2021 at 15:48):Kleiton Pereira posted a new question on April 14, 2021 at 05:40PM: coq - Unable to unify "None = Some x" with "Some (f x) = None" – stackoverflow.com
StackExchange Bot (Apr 15 2021 at 03:48):zeesha huq posted a new question on April 15, 2021 at 04:48AM: Use of build-In function in Coq – stackoverflow.com
StackExchange Bot (Apr 16 2021 at 18:48):domino posted a new question on April 16, 2021 at 08:16PM: Coq: Functions for finding the lightest weight edge. Error msg – stackoverflow.com
StackExchange Bot (Apr 17 2021 at 12:48):zeesha huq posted a new question on April 17, 2021 at 01:56PM: Counting of natural numbers in the list – stackoverflow.com
StackExchange Bot (Apr 18 2021 at 19:48):domino posted a new question on April 18, 2021 at 09:29PM: Is there anyway I can output all the shortest path in Coq? – stackoverflow.com
StackExchange Bot (Apr 19 2021 at 09:48):ieja posted a new question on April 19, 2021 at 10:59AM: MApp subgoal in Pumping lemma – stackoverflow.com
StackExchange Bot (Apr 19 2021 at 10:48):ieja posted a new question on April 19, 2021 at 12:33PM: Pumping lemma MStarApp case – stackoverflow.com
StackExchange Bot (Apr 20 2021 at 10:48):R. Bosman posted a new question on April 20, 2021 at 12:25PM: (genralized) rewriting of an equivalent term under constructor? – stackoverflow.com
StackExchange Bot (Apr 20 2021 at 10:48):ieja posted a new question on April 20, 2021 at 12:25PM: Coq proving addition inequality – stackoverflow.com
StackExchange Bot (Apr 20 2021 at 14:48):user7508402 posted a new question on April 20, 2021 at 03:56PM: Coq: rewriting under if-then-else – stackoverflow.com
StackExchange Bot (Apr 20 2021 at 17:48):Houda posted a new question on April 20, 2021 at 07:29PM: Cannot find a physical path bound to logical path matching suffix <> and prefix Coquelicot – stackoverflow.com
StackExchange Bot (Apr 21 2021 at 21:48):abeln posted a new question on April 21, 2021 at 10:56PM: Trigger typeclass search from auto/eauto – stackoverflow.com
StackExchange Bot (Apr 26 2021 at 21:48):Vaibhav G. posted a new question on April 26, 2021 at 11:17PM: How to represent kleisli composition of substitutions in abstract trees – stackoverflow.com
StackExchange Bot (Apr 27 2021 at 13:48):ieja posted a new question on April 27, 2021 at 03:43PM: Coq ssreflect sum of sums – stackoverflow.com
StackExchange Bot (Apr 27 2021 at 18:48):Fusen posted a new question on April 27, 2021 at 08:39PM: Compare sums ssreflect – stackoverflow.com
StackExchange Bot (Apr 27 2021 at 22:48):Kathy posted a new question on April 28, 2021 at 12:18AM: Rbar_le x 0 -> Rbar_le y 0 -> Rbar_le (Rbar_plus x y) 0 in Coq – stackoverflow.com
StackExchange Bot (Apr 28 2021 at 11:48):Fusen posted a new question on April 28, 2021 at 12:52PM: Ssreflect probabilities (event and not event) sum to one – stackoverflow.com
StackExchange Bot (Apr 29 2021 at 20:48):Karlo Kampić posted a new question on April 29, 2021 at 10:27PM: How to destruct a function (like H : ~ (forall x : X, p x)) in Coq? – stackoverflow.com
StackExchange Bot (Apr 29 2021 at 21:51):Kathy posted a new question on April 28, 2021 at 12:18AM: Rbar / Rbar_le / coquelicot lemma – stackoverflow.com
StackExchange Bot (Apr 30 2021 at 20:48):domino posted a new question on April 30, 2021 at 10:45PM: How to prove a odd number is the successor of double of nat in coq? – stackoverflow.com
StackExchange Bot (May 01 2021 at 04:48):domino posted a new question on May 01, 2021 at 06:24AM: Is it possible to prove oddb 0 = true?? coq – stackoverflow.com
StackExchange Bot (May 01 2021 at 13:48):DeeDee posted a new question on May 01, 2021 at 02:58PM: Using a theorem on integer numbers for proving a theorem on natural numbers – stackoverflow.com
StackExchange Bot (May 03 2021 at 10:48):VinaLx posted a new question on May 03, 2021 at 12:18PM: What does Control.refine do in Ltac2? – stackoverflow.com
StackExchange Bot (May 04 2021 at 05:48):joshan beha posted a new question on May 04, 2021 at 07:26AM: less or equal relation with largest element of natural number list – stackoverflow.com
StackExchange Bot (May 11 2021 at 22:48):David posted a new question on May 12, 2021 at 12:42AM: How to prove (~Q -> ~P) - > (P -> Q) in Coq – stackoverflow.com
StackExchange Bot (May 14 2021 at 08:48):Doyun Nam posted a new question on May 14, 2021 at 10:29AM: What does "eq^~" mean in Coq? – stackoverflow.com
StackExchange Bot (May 16 2021 at 16:48):Giacomo Maletto posted a new question on May 16, 2021 at 06:37PM: Can a function argument be scoped automatically in Coq? – stackoverflow.com
StackExchange Bot (May 17 2021 at 08:48):jayven posted a new question on May 17, 2021 at 10:19AM: Don't understand destruct tactic on hypothesis ~ (exists x : X, ~ P x) in Coq – stackoverflow.com
StackExchange Bot (May 17 2021 at 11:48):TalionZz posted a new question on May 17, 2021 at 01:32PM: Solving a mergesort split proof in Coq – stackoverflow.com
StackExchange Bot (May 21 2021 at 10:48):user1535186 posted a new question on May 21, 2021 at 12:11PM: The type checker's behavior while pattern matching in Coq – stackoverflow.com
StackExchange Bot (May 22 2021 at 18:48):Mickey Mouse posted a new question on May 22, 2021 at 08:27PM: Definitions in Coq – stackoverflow.com
StackExchange Bot (May 22 2021 at 23:48):Cris Teller posted a new question on May 23, 2021 at 01:25AM: Strong specification in Coq – stackoverflow.com
StackExchange Bot (May 23 2021 at 07:48):user4035 posted a new question on May 23, 2021 at 08:50AM: Is it possible to keep the original hypothesis while using intro pattern – stackoverflow.com
StackExchange Bot (May 23 2021 at 15:48):Cris Teller posted a new question on May 23, 2021 at 05:20PM: Inductive haskell's Replicate function in Coq – stackoverflow.com
StackExchange Bot (May 23 2021 at 16:48):Cris Teller posted a new question on May 23, 2021 at 05:20PM: Coq: Strong specification of haskell's Replicate function – stackoverflow.com
StackExchange Bot (May 24 2021 at 00:48):Cris Teller posted a new question on May 24, 2021 at 02:35AM: Coq - Proof of list pair – stackoverflow.com
StackExchange Bot (May 24 2021 at 02:48):push33n posted a new question on May 24, 2021 at 04:16AM: how to simplify basic arithmetic in more complex goals – stackoverflow.com
StackExchange Bot (May 24 2021 at 13:48):Cris Teller posted a new question on May 24, 2021 at 03:03PM: Coq: Prove Inductive relation (vs Fixpoint) – stackoverflow.com
StackExchange Bot (May 25 2021 at 16:48):Mickey Mouse posted a new question on May 25, 2021 at 06:42PM: Dealing with and sign in goal – stackoverflow.com
StackExchange Bot (May 28 2021 at 18:48):joshan beha posted a new question on May 28, 2021 at 08:08PM: How to find minimum element of natural number list – stackoverflow.com
StackExchange Bot (May 30 2021 at 06:48):Serene posted a new question on May 30, 2021 at 07:52AM: Coq: Recursive definition of fibonacci is ill-formed – stackoverflow.com
StackExchange Bot (Jun 04 2021 at 16:48):Kathy posted a new question on June 04, 2021 at 06:02PM: How to give the simple function its formula as a linear combination of indicator functions in Coq – stackoverflow.com
StackExchange Bot (Jun 09 2021 at 13:48):Eben Kadile posted a new question on June 09, 2021 at 03:37PM: Produce a function in Coq which outputs every witness to an existence-uniqueness axiom – stackoverflow.com
StackExchange Bot (Jun 11 2021 at 12:48):Saad posted a new question on June 11, 2021 at 02:39PM: True and False values of type Prop in Coq – stackoverflow.com
StackExchange Bot (Jun 12 2021 at 12:48):Yosuke Ito posted a new question on June 12, 2021 at 02:16PM: Is there any way to rewrite the function in "is_lim"? – stackoverflow.com
StackExchange Bot (Jun 13 2021 at 16:48):Cris Teller posted a new question on June 13, 2021 at 06:24PM: Coq: Cannot guess decreasing argument of fix – stackoverflow.com
StackExchange Bot (Jun 13 2021 at 21:48):Joshua Meyers posted a new question on June 13, 2021 at 10:01PM: Why does Record forget which arguments are implicit? – stackoverflow.com
StackExchange Bot (Jun 15 2021 at 11:48):Attila Karoly posted a new question on June 15, 2021 at 12:52PM: Is this a correct application of 'exists' in Coq? – stackoverflow.com
StackExchange Bot (Jun 15 2021 at 14:48):Tekkno posted a new question on June 15, 2021 at 03:26PM: How to generate Coq files from Frama-C WP plugin – stackoverflow.com
StackExchange Bot (Jun 17 2021 at 18:48):Felipe posted a new question on June 17, 2021 at 08:13PM: Composing sumbools for container type – stackoverflow.com
StackExchange Bot (Jun 18 2021 at 01:48):joshan beha posted a new question on June 18, 2021 at 03:31AM: How I can convert the relation between two terms in Coq – stackoverflow.com
StackExchange Bot (Jun 18 2021 at 19:48):Cris Teller posted a new question on June 18, 2021 at 09:14PM: Coq to Why3: with notation – stackoverflow.com
Andrey Klaus (Jun 19 2021 at 07:41): StackExchange Bot (Jun 19 2021 at 07:48):Andrey posted a new question on June 19, 2021 at 09:27AM: Why unable to perform case analysis in rather simple case – stackoverflow.com
StackExchange Bot (Jun 20 2021 at 01:48):August C. posted a new question on June 20, 2021 at 02:55AM: How do I translate static void and extern void from C to x86-64? – stackoverflow.com
StackExchange Bot (Jun 20 2021 at 03:48):Felipe posted a new question on June 20, 2021 at 05:34AM: How to write a 'safe' head in coq? – stackoverflow.com
StackExchange Bot (Jun 20 2021 at 14:48):Cris Teller posted a new question on June 20, 2021 at 04:19PM: Coq to Why3: Proof of aux lemma of function correction – stackoverflow.com
StackExchange Bot (Jun 20 2021 at 14:48):Charlie Parker posted a new question on June 20, 2021 at 04:45PM: What is a concrete example of the type Set and what is the meaning of Set? – stackoverflow.com
StackExchange Bot (Jun 20 2021 at 16:48):Cris Teller posted a new question on June 18, 2021 at 11:28PM: Why3: Proof with induction – stackoverflow.com
StackExchange Bot (Jun 20 2021 at 19:48):Mickey Mouse posted a new question on June 20, 2021 at 09:07PM: question about intros [=] and intros [= <- H] – stackoverflow.com
StackExchange Bot (Jun 20 2021 at 23:48):Giwon Song posted a new question on June 21, 2021 at 01:41AM: How to add "assumed true" statements in Coq – stackoverflow.com
StackExchange Bot (Jun 21 2021 at 10:48):Giwon Song posted a new question on June 21, 2021 at 12:41PM: How to use symmetricity of an equality on Coq – stackoverflow.com
StackExchange Bot (Jun 21 2021 at 22:48):Giwon Song posted a new question on June 22, 2021 at 12:27AM: How to prove simplification of logic(A and B implies A) in Coq – stackoverflow.com
StackExchange Bot (Jun 22 2021 at 01:48):Giwon Song posted a new question on June 22, 2021 at 02:54AM: proof of adding 1 to some number changes the parity in Coq – stackoverflow.com
StackExchange Bot (Jun 22 2021 at 16:48):pjm posted a new question on June 22, 2021 at 06:21PM: Implicit arguments propagation – stackoverflow.com
StackExchange Bot (Jun 22 2021 at 16:48):Attila Karoly posted a new question on June 22, 2021 at 06:23PM: Unifying types of identical meanings – stackoverflow.com
StackExchange Bot (Jun 22 2021 at 17:48):setholopolus posted a new question on June 22, 2021 at 07:32PM: Parametrizing a Module in Coq – stackoverflow.com
StackExchange Bot (Jun 22 2021 at 17:48):setholopolus posted a new question on June 22, 2021 at 07:45PM: Alternative tactic for ssreflect's move=> – stackoverflow.com
StackExchange Bot (Jun 23 2021 at 02:48):Felipe posted a new question on June 23, 2021 at 03:56AM: Proving two-list queue in coq – stackoverflow.com
StackExchange Bot (Jun 23 2021 at 09:48):Attila Karoly posted a new question on June 23, 2021 at 11:13AM: Computational behaviour of Successor – stackoverflow.com
StackExchange Bot (Jun 23 2021 at 10:48):Berelex posted a new question on June 23, 2021 at 12:16PM: Coq - trivial induction on lists doesn't accept assumtion – stackoverflow.com
StackExchange Bot (Jun 23 2021 at 11:48):Berelex posted a new question on June 23, 2021 at 12:16PM: (SOLVED - was a goal-printing bug) Coq - trivial induction on lists doesn't accept assumtion – stackoverflow.com
StackExchange Bot (Jun 24 2021 at 01:48):joshan beha posted a new question on June 24, 2021 at 03:03AM: How to apply/use buildin function – stackoverflow.com
StackExchange Bot (Jun 24 2021 at 18:48):98189per posted a new question on June 24, 2021 at 08:35PM: How do I prove an existential goal that asks for a certain function in Coq? – stackoverflow.com
StackExchange Bot (Jun 24 2021 at 19:48):Charlie Parker posted a new question on June 24, 2021 at 08:57PM: What does the at sign @ mean in Coq - especially in the context of Gallina terms? – stackoverflow.com
StackExchange Bot (Jun 24 2021 at 23:48):Charlie Parker posted a new question on June 25, 2021 at 12:55AM: How does one print the entire contents of a proof object or Gallina terms in Coq? – stackoverflow.com
StackExchange Bot (Jun 25 2021 at 16:48):push33n posted a new question on June 25, 2021 at 06:19PM: apply ltac to subexpression of a goal – stackoverflow.com
StackExchange Bot (Jun 26 2021 at 11:48):Bob posted a new question on June 26, 2021 at 01:25PM: Can I safely assume that isomorphic types are equal? – stackoverflow.com
StackExchange Bot (Jun 28 2021 at 04:48):KingsAlpaca posted a new question on June 28, 2021 at 06:03AM: Coq datatype - pair of pair with bracket – stackoverflow.com
StackExchange Bot (Jun 28 2021 at 10:48):Y.X. posted a new question on June 28, 2021 at 12:03PM: How does the "intro ->" in Coq work on context? – stackoverflow.com
StackExchange Bot (Jun 30 2021 at 19:48):steve01 posted a new question on June 30, 2021 at 08:56PM: Why simultaneous assignment fails? – stackoverflow.com
StackExchange Bot (Jul 02 2021 at 16:48):joshan beha posted a new question on July 02, 2021 at 05:56PM: How to consider both out puts in list – stackoverflow.com
StackExchange Bot (Jul 04 2021 at 04:48):user12986714 posted a new question on July 04, 2021 at 06:08AM: Proving equivalence of two rev_append implementations – stackoverflow.com
StackExchange Bot (Jul 04 2021 at 04:48):leonaden posted a new question on July 04, 2021 at 06:32AM: Coq: Comparing an Int to a Nat in Separation Logic Foundations – stackoverflow.com
StackExchange Bot (Jul 04 2021 at 17:48):joshan beha posted a new question on July 04, 2021 at 06:52PM: Elements count in list – stackoverflow.com
StackExchange Bot (Jul 07 2021 at 04:48):Serene posted a new question on July 07, 2021 at 05:53AM: How can I replace a variable by another in coq – stackoverflow.com
StackExchange Bot (Jul 08 2021 at 05:48):12412316 posted a new question on July 08, 2021 at 07:00AM: Can any additional axiom make Coq Turing complete? – stackoverflow.com
StackExchange Bot (Jul 08 2021 at 05:48):DoubleX posted a new question on July 08, 2021 at 07:03AM: How to clear duplicated hypothesis in Coq? – stackoverflow.com
StackExchange Bot (Jul 08 2021 at 09:48):DoubleX posted a new question on July 08, 2021 at 07:03AM: How to group duplicated hypothesis in Coq? – stackoverflow.com
StackExchange Bot (Jul 09 2021 at 16:48):Hexirp posted a new question on July 09, 2021 at 06:07PM: I tried to use PHOAS in Coq to formalize a calculus with full dependent types – stackoverflow.com
StackExchange Bot (Jul 10 2021 at 06:48):Night Heron posted a new question on July 10, 2021 at 08:45AM: Frama-C 23 and Coq – stackoverflow.com
StackExchange Bot (Jul 10 2021 at 16:48):joshan beha posted a new question on July 10, 2021 at 06:12PM: Proof related to list function – stackoverflow.com
StackExchange Bot (Jul 10 2021 at 17:48):joshan beha posted a new question on July 10, 2021 at 06:12PM: How to avoid true=false condition – stackoverflow.com
StackExchange Bot (Jul 11 2021 at 03:48):Feryll posted a new question on July 11, 2021 at 05:07AM: Coq: Induction on associated variable – stackoverflow.com
StackExchange Bot (Jul 11 2021 at 10:48):Serene posted a new question on July 11, 2021 at 12:37PM: How can I replace a variable by another in coq – mathoverflow.net
StackExchange Bot (Jul 11 2021 at 17:48):joshan beha posted a new question on July 11, 2021 at 07:14PM: equality of two numbers – stackoverflow.com
StackExchange Bot (Jul 14 2021 at 12:48):Benjamin Bray posted a new question on July 14, 2021 at 02:16PM: Coq match on Hypothesis passed to Ltac tactic – stackoverflow.com
StackExchange Bot (Jul 16 2021 at 12:48):Finn posted a new question on July 16, 2021 at 02:14PM: Why does Coquelicot mess with my bullets? – stackoverflow.com
StackExchange Bot (Jul 18 2021 at 13:22):aleesha zee posted a new question on July 18, 2021 at 02:46PM: Detail of Stack overflow questions – stackoverflow.com
StackExchange Bot (Jul 21 2021 at 06:22):Wonil Lee posted a new question on July 21, 2021 at 08:18AM: Coq question. compile errors. [file-no-extension,filesystem] and grammar entry "ident" permitted "_" – stackoverflow.com
StackExchange Bot (Jul 21 2021 at 17:44):Sereja Bogolubov posted a new question on July 21, 2021 at 06:49PM: Coq + Emacs? Check can't see what is defined in the source file – stackoverflow.com
StackExchange Bot (Jul 21 2021 at 20:44):Serene posted a new question on July 21, 2021 at 10:34PM: Proving an addition function is associative using Coq – stackoverflow.com
StackExchange Bot (Jul 23 2021 at 11:44):Dave Walker posted a new question on July 23, 2021 at 01:02PM: Proving two functions are equivalent without exactly the same hypotheses – stackoverflow.com
StackExchange Bot (Jul 24 2021 at 14:44):FH35 posted a new question on July 24, 2021 at 04:24PM: How to use a theorem with a match pattern – stackoverflow.com
StackExchange Bot (Jul 27 2021 at 19:44):Sereja Bogolubov posted a new question on July 27, 2021 at 09:13PM: Coq: proving P -> ~P -> Q without contradiction tactic? – stackoverflow.com
StackExchange Bot (Jul 28 2021 at 15:47):Hexirp posted a new question on July 28, 2021 at 05:41PM: Can I define an equivalent to this using the Axiom command? – stackoverflow.com
StackExchange Bot (Aug 01 2021 at 06:44):sara lee posted a new question on August 01, 2021 at 08:22AM: Use of recursive function in Coq – stackoverflow.com
StackExchange Bot (Aug 07 2021 at 04:44):zoha ze posted a new question on August 07, 2021 at 06:20AM: How to represent mathematical function in coq – stackoverflow.com
StackExchange Bot (Aug 07 2021 at 07:47):ZhangLiao posted a new question on August 07, 2021 at 09:18AM: A question implement CPS transform in COq – cstheory.stackexchange.com
StackExchange Bot (Aug 09 2021 at 05:45):c_j_blank posted a new question on August 09, 2021 at 07:35AM: Joining trees together to create a new tree - Coq – stackoverflow.com
StackExchange Bot (Aug 11 2021 at 15:44):Sereja Bogolubov posted a new question on August 11, 2021 at 05:06PM: Coq: eliminating forall? – stackoverflow.com
StackExchange Bot (Aug 18 2021 at 16:45):user251130 posted a new question on August 18, 2021 at 05:46PM: Making coercions explicit in assumptions in Coq – stackoverflow.com
StackExchange Bot (Aug 18 2021 at 18:45):Pedro Queiroga posted a new question on August 18, 2021 at 07:53PM: How to apply in many hypothesis at once? – stackoverflow.com
StackExchange Bot (Aug 18 2021 at 20:45):Vadim Pushtaev posted a new question on August 18, 2021 at 09:21PM: Destruct hypothesis: general case – stackoverflow.com
StackExchange Bot (Aug 21 2021 at 07:44):user1953221 posted a new question on August 21, 2021 at 07:46AM: Proving equivalence of two programs expressed as different relations – stackoverflow.com
StackExchange Bot (Aug 21 2021 at 11:44):user1953221 posted a new question on August 21, 2021 at 07:46AM: Proving equivalence of two programs expressed as different types – stackoverflow.com
StackExchange Bot (Aug 22 2021 at 11:44):exchange posted a new question on August 22, 2021 at 01:01PM: Is flattening a list easier in dependently typed functional programming languages? – stackoverflow.com
StackExchange Bot (Aug 24 2021 at 17:44):Shiranai posted a new question on August 24, 2021 at 06:49PM: Idempotency of normalizing a binary number in coq – stackoverflow.com
StackExchange Bot (Aug 25 2021 at 17:44):ZhangLiao posted a new question on August 25, 2021 at 07:35PM: How to know the number of isomorphisms in formal libraries? – cstheory.stackexchange.com
StackExchange Bot (Aug 26 2021 at 06:44):Hexirp posted a new question on August 26, 2021 at 08:12AM: Can I prove "coinductive principles" about coinductive type? – stackoverflow.com
StackExchange Bot (Aug 27 2021 at 12:44):ZhangLiao posted a new question on August 27, 2021 at 02:02PM: Is there a formal libray can show how many times a specified symbols appear in the library? – cstheory.stackexchange.com
StackExchange Bot (Aug 27 2021 at 19:47):santker heboln posted a new question on August 27, 2021 at 08:43PM: Definition of Category and internal category in coq – stackoverflow.com
StackExchange Bot (Aug 30 2021 at 23:45):Henry Zhang posted a new question on August 31, 2021 at 01:43AM: In Coq how to combine two hypothesis or rearrange the parenthesis in subgoals – stackoverflow.com
StackExchange Bot (Aug 31 2021 at 22:47):Grant Jurgensen posted a new question on September 01, 2021 at 12:16AM: Why can't Coq infer my coercion when applying arguments to coercible term? – stackoverflow.com
StackExchange Bot (Sep 02 2021 at 18:45):pjm posted a new question on September 02, 2021 at 06:50PM: Combine implicit arguments and partial application – stackoverflow.com
StackExchange Bot (Sep 05 2021 at 06:44):scubed posted a new question on September 05, 2021 at 08:05AM: The missing De Morgan's law – stackoverflow.com
StackExchange Bot (Sep 05 2021 at 15:44):user566206 posted a new question on September 05, 2021 at 04:27PM: How can I prove add_le_cases (forall n m p q, n + m <= p + q -> n <= p \/ m <= q) – stackoverflow.com
StackExchange Bot (Sep 05 2021 at 20:44):NotAPlane posted a new question on September 05, 2021 at 10:20PM: New to Coq: How to compile .vo files and run command line? – stackoverflow.com
StackExchange Bot (Sep 06 2021 at 22:44):Andrew Au posted a new question on September 07, 2021 at 12:26AM: Annotating Coq proofs – stackoverflow.com
StackExchange Bot (Sep 07 2021 at 07:44):Andrey posted a new question on September 07, 2021 at 09:42AM: What the data type does author mean in exercises for cpdt book? – stackoverflow.com
StackExchange Bot (Sep 08 2021 at 11:44):Kristian posted a new question on September 08, 2021 at 12:17PM: Adding "in" part to tactic to specify where to apply it – stackoverflow.com
StackExchange Bot (Sep 08 2021 at 13:44):Abastro posted a new question on September 08, 2021 at 02:49PM: Proof irrelevance of decidable *inequality* in coq – stackoverflow.com
StackExchange Bot (Sep 08 2021 at 13:44):Serene M posted a new question on September 08, 2021 at 02:53PM: How to prove list concatenation is not commutative using coq? – stackoverflow.com
StackExchange Bot (Sep 08 2021 at 23:44):Serene M posted a new question on September 09, 2021 at 12:56AM: Error message: Not the right number of missing arguments (expected 1) – stackoverflow.com
StackExchange Bot (Sep 10 2021 at 23:44):Kristian posted a new question on September 11, 2021 at 12:48AM: Problems with missing information in Obligations when defining using Program in Coq – stackoverflow.com
StackExchange Bot (Sep 11 2021 at 15:44):user566206 posted a new question on September 11, 2021 at 05:21PM: Proving MStar' in Logical Foundations (IndProp.v) – stackoverflow.com
StackExchange Bot (Sep 13 2021 at 00:44):Serene M posted a new question on September 13, 2021 at 02:20AM: An assumption in the goal is completely the same with a function I defined beforehand. How can I tell Coq they are indeed the same? – stackoverflow.com
StackExchange Bot (Sep 13 2021 at 20:44):Kristian posted a new question on September 13, 2021 at 08:49PM: Add notation to a scope globally in Coq – stackoverflow.com
StackExchange Bot (Sep 13 2021 at 20:44):Felipe Balbi posted a new question on September 13, 2021 at 08:52PM: Binary tree inversion in Coq – stackoverflow.com
StackExchange Bot (Sep 15 2021 at 08:44):Fusen posted a new question on September 15, 2021 at 10:33AM: VSCoq ProofView not printing – stackoverflow.com
StackExchange Bot (Sep 16 2021 at 14:44):Andrey posted a new question on September 16, 2021 at 04:10PM: ssreflect inversion, I need two equations instead of one – stackoverflow.com
StackExchange Bot (Sep 17 2021 at 20:44):paulotorrens posted a new question on September 17, 2021 at 10:20PM: Is it possible to turn unification errors into goals in Coq? – stackoverflow.com
StackExchange Bot (Sep 19 2021 at 22:44):Rupert Swarbrick posted a new question on September 20, 2021 at 12:40AM: Trying to define a "rect2"-like function on heterogeneous vectors – stackoverflow.com
StackExchange Bot (Sep 20 2021 at 05:44):Serene M posted a new question on September 20, 2021 at 07:09AM: Error: Cannot interpret this number as a value of type nat – stackoverflow.com
StackExchange Bot (Sep 20 2021 at 06:44):Felipe Balbi posted a new question on September 20, 2021 at 07:56AM: Software Foundations Volume 1: Tactics: injection_ex3 – stackoverflow.com
StackExchange Bot (Sep 21 2021 at 05:44):KaisoHHH posted a new question on September 21, 2021 at 06:33AM: Coq proof for a regular expression on boolean value – stackoverflow.com
StackExchange Bot (Sep 23 2021 at 11:44):Kristian posted a new question on September 23, 2021 at 12:58PM: Avoid dulicating code for applying tactics in both hypothesis and goal – stackoverflow.com
StackExchange Bot (Sep 24 2021 at 08:44):Kristian posted a new question on September 23, 2021 at 12:58PM: Avoid duplicating code for applying tactics in both hypothesis and goal – stackoverflow.com
StackExchange Bot (Sep 24 2021 at 21:44):Grant Jurgensen posted a new question on September 24, 2021 at 10:56PM: How does axiom K contradict univalence? – cstheory.stackexchange.com
StackExchange Bot (Sep 25 2021 at 17:44):geckos posted a new question on September 25, 2021 at 06:42PM: How to generalize a variable on both sides of an equation in Coq? – stackoverflow.com
StackExchange Bot (Sep 27 2021 at 09:44):Jan Tušil posted a new question on September 27, 2021 at 11:40AM: Coq unshelve in LTac2 – stackoverflow.com
StackExchange Bot (Sep 27 2021 at 17:44):Jason Gross posted a new question on September 27, 2021 at 07:17PM: Coq/SSReflect: standard way to case on (x < y) + (x == y) + (y < x)? – stackoverflow.com
StackExchange Bot (Sep 27 2021 at 20:44):dd21 posted a new question on September 27, 2021 at 09:11PM: how to prove x + n = y + n -> x = y in coq – stackoverflow.com
StackExchange Bot (Sep 28 2021 at 01:44):azani posted a new question on September 28, 2021 at 03:01AM: Can't figure out why re-write does not work – stackoverflow.com
StackExchange Bot (Sep 28 2021 at 11:44):Felipe Balbi posted a new question on September 28, 2021 at 01:32PM: SF Volume 1: Logic: How to prove tr_rev <-> rev? – stackoverflow.com
StackExchange Bot (Sep 29 2021 at 10:44):Felipe Balbi posted a new question on September 29, 2021 at 12:17PM: How to split equality of two lists? – stackoverflow.com
StackExchange Bot (Oct 01 2021 at 14:44):Tyler's ruler posted a new question on October 01, 2021 at 04:32PM: How to prove this DeMorgan law without using automation tactics in Coq? – stackoverflow.com
StackExchange Bot (Oct 01 2021 at 17:44):Felipe Balbi posted a new question on October 01, 2021 at 07:17PM: How to tell Coq that it's okay to remove the ns? – stackoverflow.com
StackExchange Bot (Oct 02 2021 at 05:44):OrenIshShalom posted a new question on October 02, 2021 at 06:52AM: Equal implies Less-Than-Or-Equal in Coq – stackoverflow.com
StackExchange Bot (Oct 02 2021 at 18:44):azani posted a new question on October 02, 2021 at 08:23PM: How can I get C-c C-n to format the current line in proof-general coq-mode-map – stackoverflow.com
StackExchange Bot (Oct 03 2021 at 16:44):Proof-By-Sledgehammer posted a new question on October 03, 2021 at 05:54PM: Suppress Warning At Import – stackoverflow.com
StackExchange Bot (Oct 04 2021 at 07:44):Proof-By-Sledgehammer posted a new question on October 04, 2021 at 09:21AM: Coercion in pairs – stackoverflow.com
StackExchange Bot (Oct 04 2021 at 09:44):sweetieeee posted a new question on October 04, 2021 at 10:49AM: What does the tactic destruct do in the proof below? – stackoverflow.com
StackExchange Bot (Oct 04 2021 at 09:44):Felipe Balbi posted a new question on October 04, 2021 at 11:42AM: How to prove plus_le_compat_l : forall n m p, n <= m -> p + n <= p + m. – stackoverflow.com
StackExchange Bot (Oct 05 2021 at 12:44):Felipe Balbi posted a new question on October 05, 2021 at 02:03PM: How to prove Theorem plus_lt : forall n1 n2 m, n1 + n2 < m -> n1 < m /\ n2 < m – stackoverflow.com
StackExchange Bot (Oct 05 2021 at 21:44):Matthew Gregoire posted a new question on October 05, 2021 at 10:23PM: How to express that one element of an inductive relation can't be derived from another in Coq? – stackoverflow.com
StackExchange Bot (Oct 05 2021 at 22:45):Sami Liedes posted a new question on October 06, 2021 at 12:05AM: Weird goal Some 0 = true generated in proof – stackoverflow.com
StackExchange Bot (Oct 05 2021 at 23:44):inmessionante posted a new question on October 06, 2021 at 01:00AM: proof tactics in coq can replace inversion – stackoverflow.com
StackExchange Bot (Oct 07 2021 at 08:44):Bob posted a new question on October 07, 2021 at 10:29AM: Not pretty-printing a field of a record – stackoverflow.com
StackExchange Bot (Oct 10 2021 at 14:44):Felipe Balbi posted a new question on October 10, 2021 at 04:08PM: Software Foundations: weak_pumping lemma proof – stackoverflow.com
StackExchange Bot (Oct 12 2021 at 13:44):chen yu posted a new question on October 12, 2021 at 02:57PM: Can any one help me how to prove this therom in coq – stackoverflow.com
StackExchange Bot (Oct 13 2021 at 14:45):dkutlesic posted a new question on October 13, 2021 at 03:17PM: COQ: How to use "<=" for Z and R in the same lemma? – stackoverflow.com
StackExchange Bot (Oct 16 2021 at 22:44):geckos posted a new question on October 16, 2021 at 11:50PM: How to apply an axiom to simplify a match in Coq? – stackoverflow.com
StackExchange Bot (Oct 17 2021 at 18:44):Chloe posted a new question on October 17, 2021 at 08:28PM: Coq stuck on proof for Theorem eqblist_true – cs.stackexchange.com
StackExchange Bot (Oct 18 2021 at 14:44):ged posted a new question on October 18, 2021 at 04:35PM: Proving that s-expressions printing is injective – stackoverflow.com
StackExchange Bot (Oct 19 2021 at 13:44):Proof-By-Sledgehammer posted a new question on October 19, 2021 at 03:04PM: Coercions of bitvectors – stackoverflow.com
StackExchange Bot (Oct 19 2021 at 16:44):qbn qsj posted a new question on October 19, 2021 at 05:45PM: Proof in Coq with named parameters in constructors – stackoverflow.com
StackExchange Bot (Oct 20 2021 at 15:44):Audition posted a new question on October 20, 2021 at 03:50PM: Coq Error: Illegal application (Non-functional construction) – stackoverflow.com
StackExchange Bot (Oct 21 2021 at 02:44):geckos posted a new question on October 21, 2021 at 04:03AM: How to do induction on BinNums.Z in Coq/ – stackoverflow.com
StackExchange Bot (Oct 21 2021 at 08:44):Proof-By-Sledgehammer posted a new question on October 21, 2021 at 10:33AM: Why does an "only printing" notation modify the parser – stackoverflow.com
StackExchange Bot (Oct 22 2021 at 22:44):Bruno posted a new question on October 23, 2021 at 12:39AM: Real numbers in Coq – stackoverflow.com
StackExchange Bot (Oct 25 2021 at 15:44):Kristian posted a new question on October 25, 2021 at 05:03PM: Decidable equality statement with Set vs. Prop – stackoverflow.com
StackExchange Bot (Oct 27 2021 at 12:44):dkutlesic posted a new question on October 27, 2021 at 02:25PM: COQ: a_j <= b_j => sum (a_j) <= sum (b_j) – stackoverflow.com
StackExchange Bot (Oct 27 2021 at 16:44):dkutlesic posted a new question on October 27, 2021 at 02:25PM: Proving a_j ≤ b_j → sum (a_j) ≤ sum (b_j) – stackoverflow.com
StackExchange Bot (Oct 28 2021 at 09:44):Vaishnavi Lakkalkatti ee17b065 posted a new question on October 28, 2021 at 11:35AM: Modulo simplification in coq – stackoverflow.com
StackExchange Bot (Oct 29 2021 at 09:44):Proof-By-Sledgehammer posted a new question on October 29, 2021 at 09:51AM: Implicit parameter in singleton class – stackoverflow.com
StackExchange Bot (Oct 29 2021 at 19:44):Grant Jurgensen posted a new question on October 29, 2021 at 09:21PM: Is CoInductive "extensionality" sound in Coq? Is it generalizable? – stackoverflow.com
StackExchange Bot (Oct 30 2021 at 10:44):Proof-By-Sledgehammer posted a new question on October 30, 2021 at 10:56AM: state monad on field of record – stackoverflow.com
StackExchange Bot (Nov 01 2021 at 14:44):Sebastian Fisher posted a new question on November 01, 2021 at 02:30PM: Transitivity of subsequence in COQ – stackoverflow.com
StackExchange Bot (Nov 02 2021 at 18:44):pjm posted a new question on November 02, 2021 at 06:11PM: Coinductive principle for streams – stackoverflow.com
StackExchange Bot (Nov 03 2021 at 08:44):LogicChains posted a new question on November 03, 2021 at 07:48AM: Is "less than" for rational numbers decideable in Coq? – stackoverflow.com
StackExchange Bot (Nov 03 2021 at 09:44):joro posted a new question on November 03, 2021 at 10:12AM: Can we get contradiction in ZFC if we define $a\mod 0$? – mathoverflow.net
StackExchange Bot (Nov 05 2021 at 22:44):sdpoll posted a new question on November 05, 2021 at 10:27PM: How to try a tactic in Ltac, but continue if it fails – stackoverflow.com
StackExchange Bot (Nov 05 2021 at 22:44):sdpoll posted a new question on November 05, 2021 at 10:57PM: What is the tactic that does nothing? – stackoverflow.com
StackExchange Bot (Nov 07 2021 at 20:44):geckos posted a new question on November 07, 2021 at 09:08PM: What is the difference of induction n, m and induction n; induction m in Coq? – stackoverflow.com
StackExchange Bot (Nov 09 2021 at 03:45):nanoeng posted a new question on November 09, 2021 at 04:09AM: What's the correct setup for Kami (Coq framework for Bluespec) to be able to run on WSL Ubuntu? – stackoverflow.com
StackExchange Bot (Nov 10 2021 at 17:45):John Regis posted a new question on November 10, 2021 at 06:41PM: Coq: How to prove that forall n m, n <= m \/ m <= n – stackoverflow.com
StackExchange Bot (Nov 11 2021 at 13:44):ged posted a new question on November 11, 2021 at 01:10PM: Unification problem with HOL-style alpha-conversion in Coq (matching the equality) – stackoverflow.com
StackExchange Bot (Nov 12 2021 at 14:44):Damián Ferencz posted a new question on November 12, 2021 at 03:05PM: Is it possible to declare type-dependent Notation in Coq? – stackoverflow.com
StackExchange Bot (Nov 12 2021 at 22:46):sdpoll posted a new question on November 12, 2021 at 10:57PM: How to replace a term with some property of the term? – stackoverflow.com
StackExchange Bot (Nov 13 2021 at 18:44):მამუკა ჯიბლაძე posted a new question on November 13, 2021 at 05:46PM: Coq seemingly refuses to recognize a simple substitution of a propositional formula for a propositional variable? – stackoverflow.com
StackExchange Bot (Nov 15 2021 at 17:44):calcert posted a new question on November 15, 2021 at 05:27PM: Certified calculations in a proof assistant – stackoverflow.com
StackExchange Bot (Nov 17 2021 at 04:45):Sebastian Fisher posted a new question on November 17, 2021 at 04:04AM: Is there a more elegant way to convince coq that a list based hypothesis is a contradiction? – stackoverflow.com
StackExchange Bot (Nov 17 2021 at 08:44):Walter Schulze posted a new question on November 17, 2021 at 09:03AM: Mutually Recursive Function to Compare Trees – stackoverflow.com
StackExchange Bot (Nov 17 2021 at 21:44):sdpoll posted a new question on November 17, 2021 at 08:46PM: How does the Info vernacular command work? – stackoverflow.com
StackExchange Bot (Nov 17 2021 at 21:44):sdpoll posted a new question on November 17, 2021 at 10:11PM: How can I reorder existential variables in Coq? – stackoverflow.com
StackExchange Bot (Nov 19 2021 at 22:45):Dan Arnon posted a new question on November 19, 2021 at 11:25PM: Why does Coq restrict Inductive-Recursive definitions, and how is this related to Inaccessible cardinals? – mathoverflow.net
StackExchange Bot (Nov 20 2021 at 09:44):Dan Arnon posted a new question on November 19, 2021 at 11:25PM: Why does Coq restrict Inductive definitions, and how is this related to Inaccessible cardinals? – mathoverflow.net
StackExchange Bot (Nov 20 2021 at 17:44):Ember Edison posted a new question on November 20, 2021 at 05:59PM: constructive Scott's trick – stackoverflow.com
StackExchange Bot (Nov 23 2021 at 15:44):Musher Soccoli posted a new question on November 23, 2021 at 04:20PM: Equality between two propositions nat -> nat – stackoverflow.com
StackExchange Bot (Nov 23 2021 at 17:46):Musher Soccoli posted a new question on November 23, 2021 at 06:06PM: Good way of testing a class in Coq – stackoverflow.com
StackExchange Bot (Nov 24 2021 at 20:44):Jan Tušil posted a new question on November 24, 2021 at 09:24PM: Controlling unification order in Coq – stackoverflow.com
StackExchange Bot (Nov 25 2021 at 14:44):Musher Soccoli posted a new question on November 25, 2021 at 03:33PM: Difference between parameters and conditions of a class – stackoverflow.com
StackExchange Bot (Nov 25 2021 at 16:45):Musher Soccoli posted a new question on November 25, 2021 at 03:33PM: Difference between parameters and members of a class – stackoverflow.com
StackExchange Bot (Nov 28 2021 at 07:44):მამუკა ჯიბლაძე posted a new question on November 28, 2021 at 06:56AM: Coq: a vicious circle with two identical subgoals – stackoverflow.com
StackExchange Bot (Nov 29 2021 at 16:44):John Regis posted a new question on November 29, 2021 at 05:07PM: Solving a split proof in Coq – stackoverflow.com
StackExchange Bot (Nov 29 2021 at 19:44):John Regis posted a new question on November 29, 2021 at 07:30PM: Select_perm' lemma – stackoverflow.com
StackExchange Bot (Nov 29 2021 at 20:44):Musher Soccoli posted a new question on November 29, 2021 at 09:27PM: Unable to split a conjunction in Hypothesis – stackoverflow.com
StackExchange Bot (Nov 30 2021 at 19:44):Musher Soccoli posted a new question on November 30, 2021 at 07:02PM: How to proove that all elements in a list are smaller than a given element in coq – stackoverflow.com
StackExchange Bot (Dec 01 2021 at 01:44):geckos posted a new question on December 01, 2021 at 12:53AM: How can I proove 0 <= a < b -> rem a b = a in Coq? – stackoverflow.com
StackExchange Bot (Dec 01 2021 at 20:44):Musher Soccoli posted a new question on December 01, 2021 at 09:36PM: Proving existance by providing an example – stackoverflow.com
StackExchange Bot (Dec 02 2021 at 17:44):Musher Soccoli posted a new question on December 02, 2021 at 06:41PM: Proof with multiple cases theorem – stackoverflow.com
StackExchange Bot (Dec 05 2021 at 18:44):Abcdef posted a new question on December 05, 2021 at 07:02PM: Issue with setting up Coq on VScode, "You don't have an extension for debugging Coq" – stackoverflow.com
StackExchange Bot (Dec 08 2021 at 12:44):Huan Sun posted a new question on December 08, 2021 at 01:21PM: can't launch CoqIde – stackoverflow.com
StackExchange Bot (Dec 08 2021 at 17:44):nanoeng posted a new question on December 08, 2021 at 05:50PM: Problems generating *.vos file due to CoQ Tatic failure (reversible 1st order mode) and wrong bullet – stackoverflow.com
StackExchange Bot (Dec 09 2021 at 02:45):Huan Sun posted a new question on December 09, 2021 at 03:09AM: How to Import Coq library HoTT in CoqIde – stackoverflow.com
StackExchange Bot (Dec 09 2021 at 13:44):luke36 posted a new question on December 09, 2021 at 02:18PM: Reversing a vector in Coq – stackoverflow.com
StackExchange Bot (Dec 11 2021 at 23:44):dgan posted a new question on December 11, 2021 at 11:14PM: Are those two proofs equivalent? – stackoverflow.com
StackExchange Bot (Dec 12 2021 at 16:44):Charlie Parker posted a new question on December 12, 2021 at 04:02PM: How to write intermediate proof statements inside Coq - similar to how in Isar one has have Statement using Lemma1, Lemma2 using auto but in Coq? – stackoverflow.com
StackExchange Bot (Dec 15 2021 at 13:44):Musher Soccoli posted a new question on December 15, 2021 at 02:07PM: Minimum of an ensemble in Coq – stackoverflow.com
StackExchange Bot (Dec 15 2021 at 14:45):Musher Soccoli posted a new question on December 15, 2021 at 02:07PM: Minimum of a set in Coq – stackoverflow.com
StackExchange Bot (Dec 15 2021 at 21:44):Musher Soccoli posted a new question on December 15, 2021 at 10:43PM: Proof with forall for a particular term – stackoverflow.com
StackExchange Bot (Dec 16 2021 at 10:44):KingsAlpaca posted a new question on December 16, 2021 at 10:58AM: Coq: Associativity of relational composition – stackoverflow.com
StackExchange Bot (Dec 17 2021 at 09:44):Musher Soccoli posted a new question on December 17, 2021 at 09:56AM: Simplify negation of inequality – stackoverflow.com
StackExchange Bot (Dec 17 2021 at 15:45):Charlie Parker posted a new question on December 17, 2021 at 04:35PM: How does one produce types (or theorems) from proof terms (programs or objects) in Coq? – stackoverflow.com
StackExchange Bot (Dec 17 2021 at 22:44):Lepticed posted a new question on December 17, 2021 at 11:03PM: Is there a shorter proof to this Coq theorem? – stackoverflow.com
StackExchange Bot (Dec 18 2021 at 10:44):Lepticed posted a new question on December 18, 2021 at 11:32AM: Proving a theorem containing not exists – stackoverflow.com
StackExchange Bot (Dec 21 2021 at 07:44):sdpoll posted a new question on December 21, 2021 at 08:03AM: What does the term "?T@{x:=t}", or a type with a question mark and at sign surrounding it mean in Coq? – stackoverflow.com
StackExchange Bot (Dec 21 2021 at 19:44):Charlie Parker posted a new question on December 21, 2021 at 08:15PM: What is the runtime/time complexity of Coq’s (Dependent) Type Inference? – cs.stackexchange.com
StackExchange Bot (Dec 21 2021 at 22:44):user615297 posted a new question on December 21, 2021 at 11:01PM: Supply exist argument COQ – stackoverflow.com
StackExchange Bot (Dec 22 2021 at 15:45):Grant Jurgensen posted a new question on December 22, 2021 at 04:39PM: Why is UIP unprovable in Coq? Why does the match construct generalize types? – stackoverflow.com
StackExchange Bot (Dec 25 2021 at 09:44):user1953221 posted a new question on December 25, 2021 at 09:52AM: Trace inclusion between program and state machine – stackoverflow.com
StackExchange Bot (Dec 25 2021 at 10:44):Jeff Li posted a new question on December 25, 2021 at 11:17AM: How can I prove excluded middle with the given hypothesis (forall P Q : Prop, (P -> Q) -> (~P \/ Q))? – stackoverflow.com
StackExchange Bot (Dec 25 2021 at 22:44):Paprika posted a new question on December 25, 2021 at 10:57PM: Understanding the intros keyword work in Coq – stackoverflow.com
StackExchange Bot (Dec 27 2021 at 00:44):dgan posted a new question on December 27, 2021 at 12:59AM: Cannot rewrite goal with assertion? – stackoverflow.com
StackExchange Bot (Dec 27 2021 at 00:44):Paprika posted a new question on December 27, 2021 at 01:40AM: Proving S (n + m) = n + (S m), how to rewrite n+1 = S(n)? – stackoverflow.com
StackExchange Bot (Dec 28 2021 at 15:44):geckos posted a new question on December 28, 2021 at 04:05PM: How can I proove forall a b, a <=? b = true -> a <=? S b = true) – stackoverflow.com
StackExchange Bot (Dec 28 2021 at 21:44):Rabbit Angstrom posted a new question on December 28, 2021 at 08:54PM: Coq & Emacs: Cannot compile Coq - No such file or directory – stackoverflow.com
StackExchange Bot (Dec 29 2021 at 00:44):geckos posted a new question on December 28, 2021 at 04:05PM: How can I proove forall a b, a <=? b = true -> a <=? S b = true in Coq – stackoverflow.com
StackExchange Bot (Dec 29 2021 at 03:44):Huan Sun posted a new question on December 29, 2021 at 03:55AM: How to understand syntax engine in Isabelle – stackoverflow.com
StackExchange Bot (Jan 01 2022 at 12:44):Mervin Macky posted a new question on January 01, 2022 at 12:53PM: Coq's proof #Coq – stackoverflow.com
StackExchange Bot (Jan 05 2022 at 13:44):geckos posted a new question on January 05, 2022 at 02:35PM: Is it possible to import a file in a proof only in Coq? – stackoverflow.com
StackExchange Bot (Jan 06 2022 at 12:44):The_Ghost posted a new question on January 06, 2022 at 01:36PM: How to prove shorter nat comparisons like 10000 > 1 for sigma types in Coq? – stackoverflow.com
StackExchange Bot (Jan 08 2022 at 00:44):sdpoll posted a new question on January 08, 2022 at 01:17AM: How can I write a tactic which works both in a goal and a hypothesis? – stackoverflow.com
StackExchange Bot (Jan 08 2022 at 05:44):Natasha Klaus posted a new question on January 08, 2022 at 06:36AM: Coq QuickChick : Making propery Checkable, Decidable, Arbitrary (Gen) – stackoverflow.com
StackExchange Bot (Jan 13 2022 at 07:44):Yu-zh posted a new question on January 13, 2022 at 07:31AM: Relations with dependent types in Coq – stackoverflow.com
StackExchange Bot (Jan 14 2022 at 18:44):Ramtin posted a new question on January 14, 2022 at 07:33PM: Why Coq does not infer the type parameter – stackoverflow.com
StackExchange Bot (Jan 16 2022 at 00:44):Sambo posted a new question on January 15, 2022 at 11:55PM: Coq - Coercion of list nat – stackoverflow.com
StackExchange Bot (Jan 18 2022 at 09:44):LittleJian posted a new question on January 18, 2022 at 09:56AM: How to prove the correction of derive on reg_exp – stackoverflow.com
StackExchange Bot (Jan 20 2022 at 03:44):Ene posted a new question on January 20, 2022 at 04:41AM: Defining functions on non-inductive types using LEM in Coq – cstheory.stackexchange.com
StackExchange Bot (Jan 20 2022 at 20:44):Breno posted a new question on January 20, 2022 at 07:58PM: How to prove an absurd rule in Coq – stackoverflow.com
StackExchange Bot (Jan 23 2022 at 04:44):Jimmy Stone posted a new question on January 23, 2022 at 04:09AM: Check cnat. and got Type return – stackoverflow.com
StackExchange Bot (Jan 23 2022 at 13:44):Roberto Ierusalimschy posted a new question on January 23, 2022 at 02:29PM: Coq: trying to use dependent induction – stackoverflow.com
StackExchange Bot (Jan 23 2022 at 14:44):Sam Li posted a new question on January 23, 2022 at 03:02PM: Addition of natural numbers in Coq – stackoverflow.com
StackExchange Bot (Jan 24 2022 at 02:44):IsAdisplayName posted a new question on January 24, 2022 at 02:47AM: Problem with Ocaml and make: "Error: the file ____.cmxa is not a compilation unit description" – stackoverflow.com
StackExchange Bot (Jan 27 2022 at 17:44):Breno posted a new question on January 27, 2022 at 04:45PM: How to prove in Coq ~~(P \/ ~P) – stackoverflow.com
StackExchange Bot (Jan 27 2022 at 21:44):user615297 posted a new question on January 27, 2022 at 09:46PM: Coq, true datatype – stackoverflow.com
StackExchange Bot (Jan 28 2022 at 13:44):french_cruller posted a new question on January 28, 2022 at 02:16PM: Proof of "less equal" transitive law in Coq – stackoverflow.com
StackExchange Bot (Jan 29 2022 at 08:44):Hexirp posted a new question on January 29, 2022 at 09:20AM: In Coq, Export, Require, and filtered_import do not work well – stackoverflow.com
StackExchange Bot (Jan 29 2022 at 21:44):IsAdisplayName posted a new question on January 29, 2022 at 09:56PM: Problems adding new notation in Coq – stackoverflow.com
StackExchange Bot (Feb 01 2022 at 19:44):Sambo posted a new question on February 01, 2022 at 08:14PM: Coq - Obtaining equality from match statement – stackoverflow.com
StackExchange Bot (Feb 03 2022 at 07:44):IsAdisplayName posted a new question on February 03, 2022 at 08:03AM: Coq rewrite tactic can't find subterm – stackoverflow.com
StackExchange Bot (Feb 05 2022 at 13:44):user615297 posted a new question on February 05, 2022 at 02:15PM: Apply and apply with COQ – stackoverflow.com
StackExchange Bot (Feb 05 2022 at 15:44):Brent Pappas posted a new question on February 05, 2022 at 03:09PM: Coq - Rewriting a FMap Within a Relation – stackoverflow.com
StackExchange Bot (Feb 05 2022 at 19:44):dgan posted a new question on February 05, 2022 at 07:13PM: Coq: Cannot infer an internal placeholder of type "nat" in environment: ev : nat -> Prop – stackoverflow.com
StackExchange Bot (Feb 07 2022 at 19:46):IsAdisplayName posted a new question on February 07, 2022 at 08:34PM: Coq: How are the equality tacticts symmetry and transitivity defined? – stackoverflow.com
StackExchange Bot (Feb 07 2022 at 21:44):IsAdisplayName posted a new question on February 07, 2022 at 08:52PM: Coq Uni Math Sigma Types Wont Bind a family of types – stackoverflow.com
StackExchange Bot (Feb 08 2022 at 14:44):Ak_Ak posted a new question on February 08, 2022 at 03:38PM: Theorem euclid_gcd , proving that forall a b z, euclid a b z -> gcd a b z. using coq – stackoverflow.com
StackExchange Bot (Feb 11 2022 at 16:44):Breno posted a new question on February 11, 2022 at 05:23PM: How to prove that another definition of permutation is the same as the Default Permutation Library for COQ – stackoverflow.com
StackExchange Bot (Feb 14 2022 at 21:44):Charlie Parker posted a new question on February 14, 2022 at 09:20PM: How does one install a new version of Coq when it cannot find the repositories in a new mac m1 machine? – stackoverflow.com
StackExchange Bot (Feb 16 2022 at 15:44):nobody posted a new question on February 16, 2022 at 03:06PM: Best practices for parametrized Coq libraries – stackoverflow.com
StackExchange Bot (Feb 18 2022 at 19:49):dgan posted a new question on February 18, 2022 at 08:33PM: "False" in goal: is that a an indication I am doing something wrong? – stackoverflow.com
StackExchange Bot (Feb 21 2022 at 12:44):Ricardo Maurizio Paul posted a new question on February 21, 2022 at 01:41PM: Coq: prove while is equivalent to repeat – stackoverflow.com
StackExchange Bot (Feb 21 2022 at 22:44):Sambo posted a new question on February 21, 2022 at 10:27PM: Coq: goal is just a type (when using theorems with unnecessary arguments) – stackoverflow.com
StackExchange Bot (Feb 22 2022 at 14:44):georgionic posted a new question on February 22, 2022 at 02:59PM: How to create a Powerset of MSetList? – stackoverflow.com
StackExchange Bot (Feb 22 2022 at 14:44):Jo Liss posted a new question on February 22, 2022 at 03:15PM: How to run SearchAbout snippet in company-coq-tutorial – stackoverflow.com
StackExchange Bot (Feb 22 2022 at 22:44):Jo Liss posted a new question on February 22, 2022 at 11:18PM: Remove useless hypothesis from context – stackoverflow.com
StackExchange Bot (Feb 24 2022 at 10:44):Natasha Klaus posted a new question on February 24, 2022 at 11:32AM: Problem with Dependent pattern matching in COQ – stackoverflow.com
StackExchange Bot (Feb 25 2022 at 14:44):7Orion7 posted a new question on February 25, 2022 at 03:39PM: Why does this Coq Definition fail? Coq Namespace error for Inductive Type – stackoverflow.com
StackExchange Bot (Feb 26 2022 at 12:44):Jimmy Stone posted a new question on February 26, 2022 at 01:24PM: Translate smtlib2 model to COQ – stackoverflow.com
StackExchange Bot (Feb 26 2022 at 15:44):Jo Liss posted a new question on February 26, 2022 at 03:51PM: Curly brace proof syntax: begin x. = { auto } y. [] – stackoverflow.com
StackExchange Bot (Feb 28 2022 at 12:44):Jo Liss posted a new question on February 28, 2022 at 01:27PM: Tactic for existential hypothesis – stackoverflow.com
StackExchange Bot (Mar 01 2022 at 20:44):nss posted a new question on March 01, 2022 at 09:24PM: how do I prove forall P Q : Prop, ((((P -> Q) -> P) -> P) -> Q) ->Q. in coq? – stackoverflow.com
StackExchange Bot (Mar 02 2022 at 02:44):Alex Nicolaou posted a new question on March 02, 2022 at 03:00AM: What causes fix to appear after unfolding? – stackoverflow.com
StackExchange Bot (Mar 02 2022 at 23:44):John Targaryen posted a new question on March 03, 2022 at 12:22AM: coq: Tactic to replace true hypothesis in 'and' statement – stackoverflow.com
StackExchange Bot (Mar 03 2022 at 20:44):Felipe Balbi posted a new question on March 03, 2022 at 09:13PM: Proving Binary Tree Properties – stackoverflow.com
StackExchange Bot (Mar 03 2022 at 20:44):Charlie Parker posted a new question on March 03, 2022 at 09:28PM: How to tell vscode where Coq is? (fixing Could not start coqtop (coqtop)) – stackoverflow.com
StackExchange Bot (Mar 04 2022 at 14:44):Charlie Parker posted a new question on March 04, 2022 at 03:11PM: How to activate the Coq messages in vscode/vscoq like in the CoqIde/jscoq? – stackoverflow.com
StackExchange Bot (Mar 04 2022 at 14:44):Charlie Parker posted a new question on March 04, 2022 at 03:18PM: What do the consecutive in's in Coq do and eval & red & Idtac do? – stackoverflow.com
StackExchange Bot (Mar 04 2022 at 19:44):Charlie Parker posted a new question on March 04, 2022 at 06:44PM: How does one automatically lint Coq files in vscode? – stackoverflow.com
StackExchange Bot (Mar 05 2022 at 15:44):Huan Sun posted a new question on March 05, 2022 at 03:18PM: Is there a way to apply the rule to a specific assumption in Isabelle? – stackoverflow.com
StackExchange Bot (Mar 07 2022 at 14:44):Alex Nicolaou posted a new question on March 07, 2022 at 03:16PM: Proving weaker exists based on forall – stackoverflow.com
StackExchange Bot (Mar 08 2022 at 00:44):Charlie Parker posted a new question on March 08, 2022 at 01:04AM: What does apply. tactic on it's own do in Coq -- i.e. without specifying a rule or hypothesis to unify the goal's conclusion with? – stackoverflow.com
StackExchange Bot (Mar 08 2022 at 02:44):Charlie Parker posted a new question on March 08, 2022 at 02:18AM: What is the right proof term so that the ssreflect tutorial work with the exact: hAiB example? – stackoverflow.com
StackExchange Bot (Mar 09 2022 at 00:44):Charlie Parker posted a new question on March 09, 2022 at 12:51AM: Why is my local coq no acting the same as standard coq e.g. as JsCoq? – stackoverflow.com
StackExchange Bot (Mar 10 2022 at 20:55):Charlie Parker posted a new question on March 10, 2022 at 09:43PM: Why does Coq remove/clear my asserted lemmas in my proof after the base case is proved? – stackoverflow.com
StackExchange Bot (Mar 11 2022 at 19:44):Sambo posted a new question on March 11, 2022 at 07:52PM: Creating Coq tactic: how to use a newly generated name? – stackoverflow.com
StackExchange Bot (Mar 12 2022 at 01:44):Kevin Flowers Jr posted a new question on March 12, 2022 at 12:49AM: Building non-classical logics in Adga & Coq – cs.stackexchange.com
StackExchange Bot (Mar 12 2022 at 17:44):F1r09 posted a new question on March 12, 2022 at 05:45PM: how to create a polymorphe couple such as "( a : type A, b : type B ) " in lambda-calculus – stackoverflow.com
StackExchange Bot (Mar 13 2022 at 18:44):Vincent Iampietro posted a new question on March 13, 2022 at 06:47PM: How to tell the Coq kernel that a parameter of a lambda function is a subterm of another variable in the scope? – stackoverflow.com
StackExchange Bot (Mar 14 2022 at 14:44):F1r09 posted a new question on March 14, 2022 at 03:21PM: Number of element in a list in lambd-calculus? – stackoverflow.com
StackExchange Bot (Mar 14 2022 at 19:44):F1r09 posted a new question on March 14, 2022 at 08:41PM: Concatenation of 2 lists in lambda-calculus – stackoverflow.com
StackExchange Bot (Mar 15 2022 at 13:44):Echo_Zero posted a new question on March 15, 2022 at 12:46PM: Warning : “Set this option from the IDE menu instead” in coq – stackoverflow.com
StackExchange Bot (Mar 15 2022 at 17:44):lyfeng posted a new question on March 10, 2022 at 05:18AM: How to set defaults for implicit arguments when they can't be inferred? – proofassistants.stackexchange.com
StackExchange Bot (Mar 15 2022 at 17:44):Gregory Nisbet posted a new question on March 12, 2022 at 02:22AM: List of general purpose Coq sublanguages for defining custom tactics – proofassistants.stackexchange.com
StackExchange Bot (Mar 15 2022 at 17:44):Walter Schulze posted a new question on March 14, 2022 at 09:05AM: Coq: Recursive Smart Constructors and Sigma types, how to avoid axioms – proofassistants.stackexchange.com
StackExchange Bot (Mar 15 2022 at 19:44):t1kumi posted a new question on March 15, 2022 at 08:35PM: reverse and insert list lambda calculus – stackoverflow.com
StackExchange Bot (Mar 16 2022 at 01:44):Kyrene posted a new question on March 16, 2022 at 01:56AM: How to prove a constant function that neither injective nor surjective in Coq? – stackoverflow.com
StackExchange Bot (Mar 16 2022 at 11:44):t1kumi posted a new question on March 15, 2022 at 08:35PM: How to reverse a list and insert an element in a list in lambda calculus? – stackoverflow.com
StackExchange Bot (Mar 16 2022 at 11:44):t1kumi posted a new question on March 16, 2022 at 11:50AM: How to reverse list in lambda calculus? – stackoverflow.com
StackExchange Bot (Mar 17 2022 at 14:44):ARevX posted a new question on March 17, 2022 at 02:52PM: Coq proof usage – stackoverflow.com
StackExchange Bot (Mar 17 2022 at 19:44):Théo Winterhalter posted a new question on March 17, 2022 at 08:00PM: Well-foundedness: classical equivalence of no infinite descent and accessibility – proofassistants.stackexchange.com
StackExchange Bot (Mar 17 2022 at 19:44):Charlie Parker posted a new question on March 17, 2022 at 08:26PM: How does one define dependent type with named arguments in Coq without issues in unification in the constructors? – stackoverflow.com
StackExchange Bot (Mar 17 2022 at 21:44):Charlie Parker posted a new question on March 17, 2022 at 09:16PM: How does one build the list of only true elements in Coq using dependent types? – stackoverflow.com
StackExchange Bot (Mar 17 2022 at 23:44):Kevin Flowers Jr posted a new question on March 12, 2022 at 12:49AM: Building non-classical logics in Agda & Coq – cs.stackexchange.com
StackExchange Bot (Mar 18 2022 at 11:44):Kyle Stemen posted a new question on March 18, 2022 at 11:48AM: For functions that are eq_dep equal, are their applications eq_dep equal without axioms? – proofassistants.stackexchange.com
StackExchange Bot (Mar 18 2022 at 18:44):Charlie Parker posted a new question on March 18, 2022 at 07:35PM: What does IH cannot be used as a hint. in Coq mean when using eauto giving it the induction hypothesis directly? – stackoverflow.com
StackExchange Bot (Mar 19 2022 at 08:44):Nicholas Weston posted a new question on March 19, 2022 at 09:02AM: Removing the last element of a sized list in Coq – stackoverflow.com
StackExchange Bot (Mar 19 2022 at 10:44):t1kumi posted a new question on March 19, 2022 at 11:34AM: Determine if a given tree is a binary search tree with lambda calculus – stackoverflow.com
StackExchange Bot (Mar 19 2022 at 14:44):Charlie Parker posted a new question on March 19, 2022 at 03:41PM: How to solve the very simple Syntax error: 'end' expected after [branches] (in [term_match]). in Coq? (in Gallina and not ltac) – stackoverflow.com
StackExchange Bot (Mar 19 2022 at 21:44):Jason Rute posted a new question on March 19, 2022 at 09:59PM: How does the formal proof of the four color theorem work? – proofassistants.stackexchange.com
StackExchange Bot (Mar 20 2022 at 11:44):Josip Pavičić posted a new question on March 20, 2022 at 12:19PM: proving surjectivity in coq – stackoverflow.com
StackExchange Bot (Mar 23 2022 at 19:44):Kyrene posted a new question on March 23, 2022 at 07:39PM: Proof constant not surjective Coq – stackoverflow.com
StackExchange Bot (Mar 23 2022 at 21:44):Molossus Spondee posted a new question on March 23, 2022 at 08:56PM: How to write heavily indexed proofs? – proofassistants.stackexchange.com
StackExchange Bot (Mar 23 2022 at 23:44):Carl Patenaude Poulin posted a new question on March 24, 2022 at 12:16AM: Coq: what does it mean to "saturate" a proof's context? – stackoverflow.com
StackExchange Bot (Mar 23 2022 at 23:44):Carl Patenaude Poulin posted a new question on March 24, 2022 at 12:28AM: Coq: easiest way to construct members of a decidable sigma type? – stackoverflow.com
StackExchange Bot (Mar 24 2022 at 19:44):Sebastian Fisher posted a new question on March 24, 2022 at 08:04PM: Coq Program Fixpoint vs equations as far as best way to get reduction lemmas? – stackoverflow.com
StackExchange Bot (Mar 26 2022 at 00:44):Breno posted a new question on March 26, 2022 at 01:20AM: How to build a proof of correctness in coq for elements_tr – stackoverflow.com
StackExchange Bot (Mar 27 2022 at 03:44):Breno posted a new question on March 27, 2022 at 04:40AM: How to prove insert_BST in Coq – stackoverflow.com
StackExchange Bot (Mar 27 2022 at 17:44):q.undertow posted a new question on March 27, 2022 at 07:26PM: Why does this trivial prrof fail with structuring tacticals? – proofassistants.stackexchange.com
StackExchange Bot (Mar 27 2022 at 19:44):q.undertow posted a new question on March 27, 2022 at 07:26PM: Why does this trivial proof fail with structuring tacticals? – proofassistants.stackexchange.com
StackExchange Bot (Mar 29 2022 at 21:45):Ende Jin posted a new question on March 29, 2022 at 09:49PM: Does Coq's Module and Functor type-check incrementally? – proofassistants.stackexchange.com
StackExchange Bot (Mar 29 2022 at 23:45):nss posted a new question on March 30, 2022 at 12:40AM: I am trying to solve constant is not surjective through coq – stackoverflow.com
StackExchange Bot (Mar 31 2022 at 18:37):Couchy posted a new question on March 31, 2022 at 07:40PM: What is the role of impredicativity in program extraction? – proofassistants.stackexchange.com
StackExchange Bot (Apr 01 2022 at 02:44):Breno posted a new question on April 01, 2022 at 04:13AM: How to solve a simple inequality in COQ with the same variable which is adding on both sides of the inequality – stackoverflow.com
StackExchange Bot (Apr 01 2022 at 10:44):Lepticed posted a new question on April 01, 2022 at 11:06AM: Using the commutativity of the AND operator in Coq – stackoverflow.com
StackExchange Bot (Apr 01 2022 at 17:44):Lepticed posted a new question on April 01, 2022 at 07:34PM: Define a function based on a relation in Coq – stackoverflow.com
StackExchange Bot (Apr 05 2022 at 23:44):sdpoll posted a new question on April 06, 2022 at 01:16AM: Using tuples when constructing inductive types – stackoverflow.com
StackExchange Bot (Apr 06 2022 at 14:44):Lepticed posted a new question on April 06, 2022 at 04:28PM: Pose proof in Coq – stackoverflow.com
StackExchange Bot (Apr 07 2022 at 20:44):Lepticed posted a new question on April 07, 2022 at 10:12PM: How to get a better proof style in Coq? – stackoverflow.com
StackExchange Bot (Apr 09 2022 at 01:44):L. F. posted a new question on April 09, 2022 at 03:07AM: Proving uniqueness of an instance of an indexed inductive type – proofassistants.stackexchange.com
StackExchange Bot (Apr 11 2022 at 19:45):Ende Jin posted a new question on April 11, 2022 at 09:25PM: Why Coq's Include is designed to instantiate functor with current interactive defining module? – proofassistants.stackexchange.com
StackExchange Bot (Apr 11 2022 at 22:45):dvr posted a new question on April 11, 2022 at 11:47PM: rewriting hypothesis to false with a contradictory theorem – stackoverflow.com
StackExchange Bot (Apr 12 2022 at 13:44):Kevin Buzzard posted a new question on April 12, 2022 at 02:53PM: Examples of formalisation of abelian categories – proofassistants.stackexchange.com
StackExchange Bot (Apr 13 2022 at 00:44):Couchy posted a new question on April 13, 2022 at 02:35AM: Defining coercion for proof irrelevant equality – proofassistants.stackexchange.com
StackExchange Bot (Apr 13 2022 at 01:44):lyfeng posted a new question on April 13, 2022 at 03:25AM: How to provide a countType when using mathcomp? – proofassistants.stackexchange.com
StackExchange Bot (Apr 13 2022 at 12:44):Tempestas Ludi posted a new question on April 13, 2022 at 02:11PM: Cannot discriminate 0 = 1 – proofassistants.stackexchange.com
StackExchange Bot (Apr 14 2022 at 16:44):lyfeng posted a new question on April 14, 2022 at 06:09PM: How to prove has_esp when using mathcomp.analysis? – proofassistants.stackexchange.com
StackExchange Bot (Apr 15 2022 at 11:44):Andrey posted a new question on April 15, 2022 at 11:52AM: setoid_rewrite: rewrite under bindings with 2 parameters – stackoverflow.com
StackExchange Bot (Apr 15 2022 at 11:44):Guy Coder posted a new question on April 15, 2022 at 01:34PM: Can someone explain Coq math-comp repositories – proofassistants.stackexchange.com
StackExchange Bot (Apr 15 2022 at 16:44):louga31 posted a new question on April 15, 2022 at 05:02PM: Problem proving a binary add function – proofassistants.stackexchange.com
StackExchange Bot (Apr 16 2022 at 10:44):Guy Coder posted a new question on April 15, 2022 at 01:34PM: Explanation of Coq math-comp repositories – proofassistants.stackexchange.com
StackExchange Bot (Apr 16 2022 at 11:44):lyfeng posted a new question on April 14, 2022 at 06:09PM: How can I prove has_esp when using mathcomp.analysis? – proofassistants.stackexchange.com
StackExchange Bot (Apr 16 2022 at 19:44):Ya Boi Spy7 posted a new question on April 16, 2022 at 08:02PM: Unfolding a sum and making it match hypotheses – stackoverflow.com
StackExchange Bot (Apr 16 2022 at 19:44):louga31 posted a new question on April 16, 2022 at 09:24PM: Coq: How to replace a function by it's body when making a proof – proofassistants.stackexchange.com
StackExchange Bot (Apr 16 2022 at 21:44):Alice posted a new question on April 16, 2022 at 10:57PM: Found a constructor of inductive type bool while a constructor of list is expected – stackoverflow.com
StackExchange Bot (Apr 17 2022 at 00:44):Alice posted a new question on April 17, 2022 at 01:06AM: How to do an inductive proof – stackoverflow.com
StackExchange Bot (Apr 17 2022 at 12:44):fyo posted a new question on April 17, 2022 at 01:39PM: Importing HoTT library in Coq – stackoverflow.com
StackExchange Bot (Apr 18 2022 at 01:44):Matty898 posted a new question on April 18, 2022 at 02:09AM: How can I to prove this theorem through induction? – stackoverflow.com
StackExchange Bot (Apr 18 2022 at 01:44):Nova Sczerin posted a new question on April 18, 2022 at 03:02AM: How can I prove this theorem with induction in Coq? – proofassistants.stackexchange.com
StackExchange Bot (Apr 18 2022 at 10:44):Ben posted a new question on April 16, 2022 at 09:24PM: How to replace a function by its body – proofassistants.stackexchange.com
StackExchange Bot (Apr 19 2022 at 04:44):geckos posted a new question on April 19, 2022 at 06:21AM: How to dependent match on a list with two elements? – stackoverflow.com
StackExchange Bot (Apr 19 2022 at 12:44):Tempestas Ludi posted a new question on April 19, 2022 at 01:21PM: Found type UU where "?T" was expected – proofassistants.stackexchange.com
StackExchange Bot (Apr 19 2022 at 14:44):Alice posted a new question on April 19, 2022 at 03:54PM: proving a binary add function – stackoverflow.com
StackExchange Bot (Apr 19 2022 at 15:44):Alice posted a new question on April 19, 2022 at 05:29PM: how to code in coq a function that sum the integers represented by the 2 lists and boolean representing a holdback? – stackoverflow.com
StackExchange Bot (Apr 19 2022 at 20:44):Alice posted a new question on April 19, 2022 at 10:15PM: multiplication of two binary numbers – stackoverflow.com
StackExchange Bot (Apr 20 2022 at 10:44):DoubleX posted a new question on April 20, 2022 at 12:32PM: Coq Qed raise a warning with admitted lemmas – stackoverflow.com
StackExchange Bot (Apr 20 2022 at 12:44):Lepticed posted a new question on April 20, 2022 at 01:52PM: Using or_comm in Coq – stackoverflow.com
StackExchange Bot (Apr 20 2022 at 20:44):Alan Audia posted a new question on April 20, 2022 at 09:31PM: Proof by contradiction in Coq – stackoverflow.com
StackExchange Bot (Apr 23 2022 at 07:44):Tempestas Ludi posted a new question on April 23, 2022 at 09:31AM: Prove equality in a record type – proofassistants.stackexchange.com
StackExchange Bot (Apr 24 2022 at 10:44):Sacchan posted a new question on April 24, 2022 at 12:23PM: How to extract the witness from exists in Coq in function notation/without destructing? – proofassistants.stackexchange.com
StackExchange Bot (Apr 24 2022 at 11:44):HTNW posted a new question on April 24, 2022 at 12:58PM: What axioms do I need to search the naturals? – proofassistants.stackexchange.com
StackExchange Bot (Apr 24 2022 at 17:45):Herbal Tea posted a new question on April 24, 2022 at 06:41PM: How to exhaust the match with in coq using something like default or or clause? – stackoverflow.com
StackExchange Bot (Apr 24 2022 at 17:45):Herbal Tea posted a new question on April 24, 2022 at 07:31PM: in coq how to assume equality of two natural numbers – stackoverflow.com
StackExchange Bot (Apr 25 2022 at 12:46):Herbal Tea posted a new question on April 25, 2022 at 02:12PM: How can i model something with persistent state in coq? – stackoverflow.com
StackExchange Bot (Apr 26 2022 at 15:44):Attila Karoly posted a new question on April 26, 2022 at 05:26PM: How proof functions are combined in Coq – stackoverflow.com
StackExchange Bot (Apr 26 2022 at 18:44):Hoshino Tented posted a new question on April 26, 2022 at 07:48PM: In Coq, is there a way to prove a premise of a hypothesis conveniently? – stackoverflow.com
StackExchange Bot (Apr 27 2022 at 07:44):Attila Karoly posted a new question on April 27, 2022 at 08:15AM: Symbolic manipulation of terms in Coq – stackoverflow.com
StackExchange Bot (Apr 27 2022 at 14:44):Shubham Sondhi posted a new question on April 27, 2022 at 04:23PM: Adding an old version of Ocaml to Opam – stackoverflow.com
StackExchange Bot (Apr 27 2022 at 22:44):Rupert Swarbrick posted a new question on April 28, 2022 at 12:09AM: Searching for a counterexample to a decidable predicate – stackoverflow.com
StackExchange Bot (Apr 28 2022 at 10:44):mudri posted a new question on April 28, 2022 at 10:46AM: How do Coq's bidirectionality hints (&) affect type checking? – proofassistants.stackexchange.com
StackExchange Bot (Apr 29 2022 at 17:46):Breno posted a new question on April 29, 2022 at 06:32PM: How to deal with division in COQ? – stackoverflow.com
StackExchange Bot (Apr 30 2022 at 17:44):azani posted a new question on April 30, 2022 at 07:19PM: How can I "specialize" a polymorphic type in Coq? – stackoverflow.com
StackExchange Bot (Apr 30 2022 at 17:44):mudri posted a new question on April 30, 2022 at 07:31PM: Tactic unification vs evarconv in Coq – proofassistants.stackexchange.com
StackExchange Bot (Apr 30 2022 at 18:47):Valdigleis posted a new question on April 30, 2022 at 08:02PM: Display style proofs using Coq – proofassistants.stackexchange.com
StackExchange Bot (May 01 2022 at 14:10):Max Kubierschky posted a new question on May 01, 2022 at 03:23PM: Calculus of (inductive) Constructions: Do inductive definitions increase proof strength? – mathoverflow.net
StackExchange Bot (May 01 2022 at 18:47):caio a posted a new question on May 01, 2022 at 08:20PM: Proof theorem about bst in coq – stackoverflow.com
StackExchange Bot (May 02 2022 at 04:44):Max Kubierschky posted a new question on May 02, 2022 at 06:21AM: Calculus of (inductive) Constructions: Do inductive definitions increase proof strength? – proofassistants.stackexchange.com
StackExchange Bot (May 02 2022 at 19:44):azani posted a new question on May 02, 2022 at 09:12PM: Why can I not apply f_equal to a hypothesis? – stackoverflow.com
StackExchange Bot (May 02 2022 at 21:44):hamid k posted a new question on May 02, 2022 at 10:31PM: Why coq doesn't use subtyping for logical or? – stackoverflow.com
StackExchange Bot (May 03 2022 at 06:44):FH35 posted a new question on May 03, 2022 at 08:30AM: Precise control of conversion in Coq – stackoverflow.com
StackExchange Bot (May 05 2022 at 22:44):Shiranai posted a new question on May 06, 2022 at 12:08AM: Proof objects in the identity type – stackoverflow.com
StackExchange Bot (May 09 2022 at 11:44):Vladimir Karavaychuk posted a new question on May 09, 2022 at 01:07PM: Coq: Recursive notations with forall quantifier – stackoverflow.com
StackExchange Bot (May 09 2022 at 19:44):mobotsar posted a new question on May 09, 2022 at 07:57PM: I'm stuck trying to prove ∀x : ℕ, 3 | (x + 5x) with Coq – proofassistants.stackexchange.com
StackExchange Bot (May 10 2022 at 11:44):FH35 posted a new question on May 10, 2022 at 01:31PM: Proof on inductive type in Coq – stackoverflow.com
StackExchange Bot (May 11 2022 at 17:44):udduu posted a new question on May 11, 2022 at 07:32PM: How can i proof by absurd with coq? – stackoverflow.com
StackExchange Bot (May 12 2022 at 09:46):FH35 posted a new question on May 12, 2022 at 10:58AM: Fail to rewrite list with app_removelast_last – stackoverflow.com
StackExchange Bot (May 13 2022 at 14:44):wdeweijer posted a new question on May 13, 2022 at 03:48PM: SSReflect tuple constructor: why not use phantom? – stackoverflow.com
StackExchange Bot (May 14 2022 at 17:44):hamid k posted a new question on May 14, 2022 at 06:46PM: Prove recursive function exists using only nat_ind – stackoverflow.com
StackExchange Bot (May 14 2022 at 19:44):wdeweijer posted a new question on May 14, 2022 at 09:08PM: SSReflect tuple constructor: why not use phantom? – proofassistants.stackexchange.com
StackExchange Bot (May 14 2022 at 19:44):Vladimir Prigodsky posted a new question on May 14, 2022 at 09:09PM: Unfolding expressions in Coq by one layer – proofassistants.stackexchange.com
StackExchange Bot (May 14 2022 at 22:44):Romain C posted a new question on May 15, 2022 at 12:12AM: Cannot apply one hypothesis to another – stackoverflow.com
StackExchange Bot (May 15 2022 at 03:44):Jimmy Stone posted a new question on May 15, 2022 at 04:49AM: Equivalence but not congruence – stackoverflow.com
StackExchange Bot (May 15 2022 at 21:44):monique posted a new question on May 15, 2022 at 10:38PM: Is it possible to check the length of two strings before pattern matching against them? – stackoverflow.com
StackExchange Bot (May 17 2022 at 09:44):FH35 posted a new question on May 17, 2022 at 11:01AM: Fail to prove a permutation property – stackoverflow.com
StackExchange Bot (May 17 2022 at 18:44):Vladimir Prigodsky posted a new question on May 17, 2022 at 07:47PM: Coq: Recursive notations with forall quantifier – proofassistants.stackexchange.com
StackExchange Bot (May 19 2022 at 04:44):147pm posted a new question on May 19, 2022 at 05:17AM: Coq make failing on Omega – stackoverflow.com
StackExchange Bot (May 19 2022 at 08:44):Lepticed posted a new question on May 19, 2022 at 09:54AM: Add an assertion and its negation to Coq – stackoverflow.com
StackExchange Bot (May 19 2022 at 15:44):Molossus Spondee posted a new question on May 18, 2022 at 06:31PM: Concrete inductive construction of a W-topos with Setoids in Coq – proofassistants.stackexchange.com
StackExchange Bot (May 19 2022 at 23:44):Herbal Tea posted a new question on May 20, 2022 at 12:04AM: How to evaluate square of a binom in coq? – stackoverflow.com
StackExchange Bot (May 20 2022 at 03:44):147pm posted a new question on May 20, 2022 at 05:23AM: The reference info was not found in the current environment – stackoverflow.com
StackExchange Bot (May 20 2022 at 06:44):Vladimir Prigodsky posted a new question on May 17, 2022 at 07:47PM: Recursive notations with forall quantifier – proofassistants.stackexchange.com
StackExchange Bot (May 20 2022 at 11:44):Herbal Tea posted a new question on May 20, 2022 at 01:15PM: is coq match statement exhaustive? – stackoverflow.com
StackExchange Bot (May 20 2022 at 11:44):Cahir7 posted a new question on May 20, 2022 at 01:28PM: Running prover in why3 ,using coq - error – stackoverflow.com
StackExchange Bot (May 21 2022 at 02:44):monique posted a new question on May 21, 2022 at 04:08AM: How do I show that if a hypothesis implies not, it's the same as saying the proposition equals false (coq)? – stackoverflow.com
StackExchange Bot (May 23 2022 at 14:44):Александр Степанов posted a new question on May 23, 2022 at 03:29PM: It is necessary to solve the problem of formal verification in "Coq" – stackoverflow.com
StackExchange Bot (May 24 2022 at 03:44):OrenIshShalom posted a new question on May 24, 2022 at 05:43AM: User defined language in pandoc code-block – stackoverflow.com
StackExchange Bot (May 24 2022 at 21:44):Kyle Stemen posted a new question on May 24, 2022 at 11:29PM: Can a Prop show that all entries of a list equal Type@{U} for any U? – proofassistants.stackexchange.com
StackExchange Bot (May 25 2022 at 10:44):Joachim Breitner posted a new question on May 25, 2022 at 12:00PM: Formal description of Coq’s termination checker – proofassistants.stackexchange.com
StackExchange Bot (May 25 2022 at 16:44):FH35 posted a new question on May 25, 2022 at 06:05PM: Can't find a way to 'reverse' a constructor – stackoverflow.com
StackExchange Bot (May 26 2022 at 10:44):Александр Степанов posted a new question on May 26, 2022 at 11:56AM: Coq. Not sure how to write the solution in Coq – stackoverflow.com
StackExchange Bot (May 26 2022 at 22:44):Michele De Pascalis posted a new question on May 26, 2022 at 11:38PM: Unfolding terms created with assert in Coq – stackoverflow.com
StackExchange Bot (May 29 2022 at 09:44):Lepticed posted a new question on May 29, 2022 at 10:15AM: Using the transitivity of equivalence to rewrite a goal – stackoverflow.com
StackExchange Bot (May 30 2022 at 10:44):Kiran Gopinathan posted a new question on May 30, 2022 at 10:53AM: How to evaluate proof terms through opaque definitions? – proofassistants.stackexchange.com
StackExchange Bot (May 31 2022 at 16:44):FH35 posted a new question on May 31, 2022 at 06:25PM: Can I prove a lemma without an additional inductive type – stackoverflow.com
StackExchange Bot (Jun 01 2022 at 08:44):zacque posted a new question on June 01, 2022 at 09:15AM: Why is my recursive definition of list_min ill-formed? – proofassistants.stackexchange.com
StackExchange Bot (Jun 01 2022 at 08:44):zacque posted a new question on June 01, 2022 at 10:23AM: Why does my previously defined function expands/computes to itself? – proofassistants.stackexchange.com
StackExchange Bot (Jun 01 2022 at 11:44):Lepticed posted a new question on June 01, 2022 at 11:59AM: Assume the negation of the goal in Coq – stackoverflow.com
StackExchange Bot (Jun 02 2022 at 21:44):Molossus Spondee posted a new question on June 02, 2022 at 11:41PM: Axiomization of Peano arithmetic in constructive first-order logic – proofassistants.stackexchange.com
StackExchange Bot (Jun 09 2022 at 20:44):Mathieu Borderé posted a new question on June 09, 2022 at 09:26PM: Coq - Assign expression to variable – stackoverflow.com
StackExchange Bot (Jun 09 2022 at 21:44):Molossus Spondee posted a new question on June 09, 2022 at 11:43PM: Why do record based inductive types with primitive projections lack an eta law? – proofassistants.stackexchange.com
StackExchange Bot (Jun 09 2022 at 23:44):Roland Coeurjoly posted a new question on June 10, 2022 at 12:30AM: How to fold simplified goal? – proofassistants.stackexchange.com
StackExchange Bot (Jun 10 2022 at 13:44):Roland Coeurjoly posted a new question on June 10, 2022 at 02:24PM: Obligation Tactic := intros. results in the Program Fixpoint with measure not being defined – proofassistants.stackexchange.com
StackExchange Bot (Jun 10 2022 at 23:44):Alex Nelson posted a new question on June 11, 2022 at 12:55AM: Coq inductive type with vector parameter lacks sufficient inductive principle – proofassistants.stackexchange.com
StackExchange Bot (Jun 11 2022 at 11:44):OrenIshShalom posted a new question on June 11, 2022 at 01:28PM: redundant eval $(opam env) needed in Dockerfile – stackoverflow.com
StackExchange Bot (Jun 11 2022 at 18:44):Charlie Parker posted a new question on June 11, 2022 at 06:46PM: How does one import the lia tactic given that the omega tactic was reprecated in Coq? – stackoverflow.com
StackExchange Bot (Jun 11 2022 at 18:44):Charlie Parker posted a new question on June 11, 2022 at 07:08PM: What is the best practice for installing external dependencies in a Coq project? – stackoverflow.com
StackExchange Bot (Jun 12 2022 at 08:44):Jimmy Stone posted a new question on June 12, 2022 at 10:17AM: How to write theorm for strong_progress not hold? – stackoverflow.com
StackExchange Bot (Jun 12 2022 at 15:44):Paul Snopov posted a new question on June 12, 2022 at 04:24PM: Question on some set theoretic problem – proofassistants.stackexchange.com
StackExchange Bot (Jun 12 2022 at 20:44):Paul Snopov posted a new question on June 12, 2022 at 04:24PM: Equational reasoning in Coq – proofassistants.stackexchange.com
StackExchange Bot (Jun 12 2022 at 22:44):learner123 posted a new question on June 13, 2022 at 12:38AM: How to define a counting function with fold in Coq? – stackoverflow.com
StackExchange Bot (Jun 13 2022 at 00:44):learner123 posted a new question on June 13, 2022 at 02:10AM: How to prove that in Coq that [split] and [combine] are inverses? – stackoverflow.com
StackExchange Bot (Jun 13 2022 at 00:44):newcoquser posted a new question on June 13, 2022 at 02:17AM: Problem with rewrite – proofassistants.stackexchange.com
StackExchange Bot (Jun 13 2022 at 08:44):learner123 posted a new question on June 13, 2022 at 02:10AM: How to prove in Coq that [split] and [combine] are inverses? – stackoverflow.com
StackExchange Bot (Jun 13 2022 at 08:44):FH35 posted a new question on June 13, 2022 at 10:03AM: Is this Lemma true in first-order intuitionistic logic? – stackoverflow.com
StackExchange Bot (Jun 13 2022 at 15:44):Paul Snopov posted a new question on June 13, 2022 at 04:08PM: Strong induction for nat in Coq – proofassistants.stackexchange.com
StackExchange Bot (Jun 13 2022 at 20:44):learner123 posted a new question on June 13, 2022 at 10:27PM: How to prove that [split] and [combine] are inverses in Coq? – proofassistants.stackexchange.com
StackExchange Bot (Jun 14 2022 at 12:45):learner123 posted a new question on June 14, 2022 at 01:05PM: How to prove in Coq these 2 theorems with [count_fold]? – proofassistants.stackexchange.com
StackExchange Bot (Jun 14 2022 at 16:45):Bolton Bailey posted a new question on June 14, 2022 at 06:31PM: Equivalent of range in Coq – proofassistants.stackexchange.com
StackExchange Bot (Jun 15 2022 at 17:50):Lepticed posted a new question on June 15, 2022 at 07:37PM: How to improve this proof? – stackoverflow.com
StackExchange Bot (Jun 19 2022 at 11:44):learner123 posted a new question on June 14, 2022 at 01:05PM: How to prove these 2 theorems with the help of the function below? – proofassistants.stackexchange.com
StackExchange Bot (Jun 21 2022 at 03:44):dvr posted a new question on June 21, 2022 at 04:52AM: Case analysis on max - ssreflect – stackoverflow.com
StackExchange Bot (Jun 22 2022 at 03:44):Huan Sun posted a new question on June 22, 2022 at 05:14AM: How to append all list or union all set in a map's image in Isabelle – stackoverflow.com
StackExchange Bot (Jun 22 2022 at 22:44):dvr posted a new question on June 22, 2022 at 11:27PM: Coq - prove that there exists a maximal element in a non empty sequence – stackoverflow.com
StackExchange Bot (Jun 23 2022 at 12:44):Daigo posted a new question on June 23, 2022 at 01:11PM: How to prove that addition is commutative for conatural numbers in Coq – proofassistants.stackexchange.com
StackExchange Bot (Jun 26 2022 at 16:44):Andrey posted a new question on June 26, 2022 at 06:02PM: dependent pattern matching – proofassistants.stackexchange.com
StackExchange Bot (Jun 27 2022 at 04:44):Emma Hudson posted a new question on June 27, 2022 at 06:15AM: Why not have Prop : Set in Coq? – proofassistants.stackexchange.com
StackExchange Bot (Jun 27 2022 at 18:44):dvr posted a new question on June 27, 2022 at 07:52PM: Coq - proving the value of the last element in a sequence – stackoverflow.com
StackExchange Bot (Jun 28 2022 at 02:44):Andrey posted a new question on June 28, 2022 at 04:19AM: dependent pattern matching 2 – proofassistants.stackexchange.com
StackExchange Bot (Jun 28 2022 at 07:44):Andrey posted a new question on June 28, 2022 at 04:19AM: dependent pattern matching and kind of inversion – proofassistants.stackexchange.com
StackExchange Bot (Jun 29 2022 at 21:44):op325 posted a new question on June 29, 2022 at 11:20PM: Prove that 1 > 1/2 in Coq – stackoverflow.com
StackExchange Bot (Jun 30 2022 at 06:44):op325 posted a new question on June 30, 2022 at 07:45AM: Evaluate constant inequation in Coq – stackoverflow.com
StackExchange Bot (Jul 01 2022 at 23:44):Nuclear Catapult posted a new question on July 02, 2022 at 12:39AM: Agda: Failed to solve the following constraints: P x <= _X_53 (blocked on _X_53) – stackoverflow.com
StackExchange Bot (Jul 02 2022 at 03:44):Jimmy Stone posted a new question on July 02, 2022 at 04:12AM: How can I write a nat in the form of term? – stackoverflow.com
StackExchange Bot (Jul 02 2022 at 22:44):user566206 posted a new question on July 02, 2022 at 11:34PM: Stuck at the MApp case in Logical Foundation's pumping lemma – stackoverflow.com
StackExchange Bot (Jul 03 2022 at 11:44):Lepticed posted a new question on July 03, 2022 at 12:02PM: Best way to make a relation associative in Coq – stackoverflow.com
StackExchange Bot (Jul 03 2022 at 17:44):nobody posted a new question on July 03, 2022 at 07:31PM: Working with non-empty lists: any obviously preferrable approach? – proofassistants.stackexchange.com
StackExchange Bot (Jul 03 2022 at 18:44):Naitik Mundra posted a new question on July 03, 2022 at 08:30PM: Making sure that the function I am using returns the correct kind of values in haskell. (i.e does not contain an error "" or similar) – stackoverflow.com
StackExchange Bot (Jul 04 2022 at 02:44):Andrey posted a new question on July 04, 2022 at 03:23AM: a bit complicated dependent pattern matching where I'm not able to apply convoy – proofassistants.stackexchange.com
StackExchange Bot (Jul 04 2022 at 10:44):nobody posted a new question on July 03, 2022 at 07:31PM: Why use records for non-empty lists rather than inductively defined non-empty lists? – proofassistants.stackexchange.com
StackExchange Bot (Jul 04 2022 at 10:44):Andrey posted a new question on July 04, 2022 at 03:23AM: How to convince Coq this dependent pattern match is exhaustive? – proofassistants.stackexchange.com
StackExchange Bot (Jul 05 2022 at 07:44):niha kee posted a new question on July 05, 2022 at 08:23AM: MAXIMUM VALUE OF THE LIST – stackoverflow.com
StackExchange Bot (Jul 07 2022 at 03:44):Jacob woolcutt posted a new question on July 07, 2022 at 04:26AM: Where is the discriminate tactic defined in Coq? – proofassistants.stackexchange.com
StackExchange Bot (Jul 07 2022 at 20:44):user566206 posted a new question on July 07, 2022 at 09:58PM: Cannot focus on a remaining unfocused goal in Coq – stackoverflow.com
Brando Miranda (Jul 08 2022 at 19:10):why wasn't this one posted here? https://proofassistants.meta.stackexchange.com/questions/214/engineerings-questions-on-internal-details-of-proof-assistant-implementations-u
Karl Palmskog (Jul 08 2022 at 19:18):the bot listens to the regular proofassistants StackExchange, and also regular StackOverflow and TCS overflow. It doesn't post meta questions.
StackExchange Bot (Jul 09 2022 at 19:44):Charlie Parker posted a new question on July 09, 2022 at 09:39PM: How does one systematically traverse OCaml representations of Coq ASTs terms? – proofassistants.stackexchange.com
StackExchange Bot (Jul 09 2022 at 20:44):Charlie Parker posted a new question on July 09, 2022 at 09:53PM: How does one access the dependent type unification algorithm from Coq's internals? – stackoverflow.com
StackExchange Bot (Jul 10 2022 at 03:44):with-forest posted a new question on July 10, 2022 at 03:57AM: A Coq question : How to prove the image of the two same valued variables under a function are same? – cstheory.stackexchange.com
StackExchange Bot (Jul 10 2022 at 17:44):wrongbyte posted a new question on July 10, 2022 at 06:54PM: Understanding how pattern matching works in Coq – stackoverflow.com
StackExchange Bot (Jul 11 2022 at 08:44):with-forest posted a new question on July 11, 2022 at 09:58AM: How to Deal with Qle_bool in the progress of proving in Coq – proofassistants.stackexchange.com
StackExchange Bot (Jul 12 2022 at 12:44):with-forest posted a new question on July 12, 2022 at 06:07AM: How to prove "$x \le y$" or "$\text{not} (x \le y)$" for rational numbers $x$ and $y$ in Coq? – proofassistants.stackexchange.com
Brando Miranda (Jul 13 2022 at 14:08):seems bot doesn't put when bounties are made? here is mine: https://stackoverflow.com/questions/72924211/how-does-one-access-the-dependent-type-unification-algorithm-from-coqs-internal
Théo Zimmermann (Jul 13 2022 at 14:55):Indeed, the bot is very limited: it just forwards the RSS feed (so only new questions are noticed).
StackExchange Bot (Jul 13 2022 at 16:44):BallBoy posted a new question on July 13, 2022 at 06:25PM: Basics of real numbers in mathcomp (Coq) – proofassistants.stackexchange.com
StackExchange Bot (Jul 14 2022 at 18:44):limitedeternity posted a new question on July 14, 2022 at 08:03PM: Proving enumerate(...) to range(len(...)) equality – stackoverflow.com
StackExchange Bot (Jul 14 2022 at 19:44):Charlie Parker posted a new question on July 14, 2022 at 09:19PM: What are Generic Arguments in Coq and how are they structured in their OCaml code? – proofassistants.stackexchange.com
StackExchange Bot (Jul 14 2022 at 21:44):Charlie Parker posted a new question on July 14, 2022 at 11:06PM: What does it mean to have no constructors in OCaml and define a type? – stackoverflow.com
StackExchange Bot (Jul 16 2022 at 00:44):Charlie Parker posted a new question on July 16, 2022 at 01:16AM: Why does TacArg accepts a value of CAst.t type when it should only accept values of types? – proofassistants.stackexchange.com
StackExchange Bot (Jul 17 2022 at 05:44):Jimmy Stone posted a new question on July 17, 2022 at 07:20AM: Encoding records in Coq – stackoverflow.com
StackExchange Bot (Jul 18 2022 at 07:44):Zazaeil posted a new question on July 18, 2022 at 09:13AM: nat -> nat uncountability proved in Coq – codereview.stackexchange.com
StackExchange Bot (Jul 18 2022 at 07:44):FH35 posted a new question on July 18, 2022 at 09:37AM: Stuck on the proof of a simple Lemma: which induction should I use? – stackoverflow.com
StackExchange Bot (Jul 18 2022 at 19:44):Leo G. posted a new question on July 18, 2022 at 07:59PM: Coq: Implementation of splitstring and proof that nothing gets deleted – stackoverflow.com
StackExchange Bot (Jul 19 2022 at 13:44):Peter LeFanu Lumsdaine posted a new question on July 19, 2022 at 02:50PM: In VSCoq, how to issue an arbitrary Gallina query via the prompt? – proofassistants.stackexchange.com
StackExchange Bot (Jul 21 2022 at 07:44):niha kee posted a new question on July 21, 2022 at 09:13AM: Holding greater or equal relation between two terms – stackoverflow.com
StackExchange Bot (Jul 22 2022 at 21:44):wrongbyte posted a new question on July 22, 2022 at 10:50PM: Why S n' =? S n' simplifies to n' =? n' in Coq? – stackoverflow.com
StackExchange Bot (Jul 23 2022 at 11:44):Ana Borges posted a new question on July 23, 2022 at 01:04PM: Has anyone accidentally "proven" a false theorem using what was later found to be a critical bug? – proofassistants.stackexchange.com
StackExchange Bot (Jul 23 2022 at 12:44):user251130 posted a new question on July 23, 2022 at 02:31PM: Decide equality with some predicate – stackoverflow.com
StackExchange Bot (Jul 24 2022 at 02:44):Kyle Stemen posted a new question on July 24, 2022 at 04:41AM: Is coercion to a higher universe injective? – proofassistants.stackexchange.com
StackExchange Bot (Jul 26 2022 at 22:44):quidproquo posted a new question on July 26, 2022 at 11:45PM: Learning Math Proof via Proof Assistants – proofassistants.stackexchange.com
StackExchange Bot (Jul 27 2022 at 20:44):Charlie Parker posted a new question on July 27, 2022 at 10:35PM: How does one compute/create a concrete/actual string in coq to pass to functions or store in a variable/identifier? – stackoverflow.com
StackExchange Bot (Jul 28 2022 at 16:44):pjm posted a new question on July 28, 2022 at 05:06PM: Coq: rewriting under a pointwise_relation – stackoverflow.com
StackExchange Bot (Jul 28 2022 at 17:44):Leo G. posted a new question on July 28, 2022 at 06:57PM: Coq: Simpl in match pattern when having an inequality hypothesis – stackoverflow.com
StackExchange Bot (Jul 29 2022 at 04:44):Naqib Zahid posted a new question on July 29, 2022 at 05:42AM: I have been stuck on MApp for pumping lemma – stackoverflow.com
StackExchange Bot (Aug 02 2022 at 07:44):with-forest posted a new question on August 02, 2022 at 09:38AM: Define a function using another function – proofassistants.stackexchange.com
StackExchange Bot (Aug 02 2022 at 09:44):钱一程 posted a new question on August 02, 2022 at 11:40AM: Unexpected coercion in constant definition – proofassistants.stackexchange.com
StackExchange Bot (Aug 02 2022 at 13:44):钱一程 posted a new question on August 02, 2022 at 11:40AM: Unexpected eta expansion in constant definition – proofassistants.stackexchange.com
StackExchange Bot (Aug 03 2022 at 03:44):with-forest posted a new question on August 03, 2022 at 05:27AM: A problem similar to intermediate value problem – proofassistants.stackexchange.com
StackExchange Bot (Aug 04 2022 at 07:44):Lepticed posted a new question on August 04, 2022 at 09:42AM: How to use a definition in Coq? – stackoverflow.com
StackExchange Bot (Aug 04 2022 at 09:45):Indprinciple posted a new question on August 04, 2022 at 11:21AM: How to instantiate non-dependent implicit arguments in Coq? – proofassistants.stackexchange.com
StackExchange Bot (Aug 04 2022 at 11:44):Indprinciple posted a new question on August 04, 2022 at 11:21AM: Non-dependent implicit argument instantiation in Coq's reference manual does not work – proofassistants.stackexchange.com
StackExchange Bot (Aug 07 2022 at 22:44):Malcolm Sharpe posted a new question on August 08, 2022 at 12:39AM: Coq: can tauto be used to prove classical tautologies? – proofassistants.stackexchange.com
StackExchange Bot (Aug 08 2022 at 01:44):scubed posted a new question on August 08, 2022 at 02:10AM: Prove equality with eq_rect without UIP – stackoverflow.com
StackExchange Bot (Aug 08 2022 at 12:44):with-forest posted a new question on August 08, 2022 at 01:30PM: Is there a method to make a hypothesis from applying two hypothesis? – proofassistants.stackexchange.com
StackExchange Bot (Aug 08 2022 at 17:44):with-forest posted a new question on August 08, 2022 at 01:30PM: Is there a tactic in Coq to make a hypothesis from applying two hypotheses? – proofassistants.stackexchange.com
StackExchange Bot (Aug 10 2022 at 03:44):with-forest posted a new question on August 10, 2022 at 04:03AM: When I destruct record, can I make a hypothesis name without 0? – proofassistants.stackexchange.com
StackExchange Bot (Aug 10 2022 at 06:44):with-forest posted a new question on August 10, 2022 at 07:09AM: Can I prove this axiom without using excluded-middle property? – proofassistants.stackexchange.com
StackExchange Bot (Aug 11 2022 at 09:44):Hao Yang posted a new question on August 11, 2022 at 11:03AM: Get stuck at the MStarApp case of Software Fundation's pumping Lemma – stackoverflow.com
StackExchange Bot (Aug 17 2022 at 06:44):with-forest posted a new question on August 17, 2022 at 08:31AM: How to define two mutually recursive functions in Coq? – proofassistants.stackexchange.com
StackExchange Bot (Aug 20 2022 at 14:44):Charlie Parker posted a new question on August 20, 2022 at 03:23PM: How does one automatically make a COQ_PROJ.opam install script automatically from a Coq Project? – stackoverflow.com
StackExchange Bot (Aug 21 2022 at 20:44):ax_fer posted a new question on August 21, 2022 at 09:58PM: Coq : replace hypothesis into implication – stackoverflow.com
StackExchange Bot (Aug 22 2022 at 03:44):with-forest posted a new question on August 22, 2022 at 03:54AM: What is the remaining goals on the shelf? – proofassistants.stackexchange.com
StackExchange Bot (Aug 24 2022 at 06:44):with-forest posted a new question on August 24, 2022 at 08:07AM: How to search only all of lemmas in a different module (in Coq)? – proofassistants.stackexchange.com
StackExchange Bot (Aug 25 2022 at 02:44):with-forest posted a new question on August 24, 2022 at 08:07AM: How can I search only all of the lemmas in a different module (in Coq)? – proofassistants.stackexchange.com
StackExchange Bot (Aug 27 2022 at 14:04):Netchaiev posted a new question on August 27, 2022 at 03:34PM: Natural deduction with coq assistant prover – proofassistants.stackexchange.com
StackExchange Bot (Aug 30 2022 at 00:47):Pietro Braione posted a new question on August 30, 2022 at 02:04AM: How do I prove this property in Coq? – proofassistants.stackexchange.com
StackExchange Bot (Aug 30 2022 at 03:54):with-forest posted a new question on August 30, 2022 at 05:27AM: How can I use a (three terms) decidable axiom in a case analysis? – proofassistants.stackexchange.com
StackExchange Bot (Aug 31 2022 at 06:44):with-forest posted a new question on August 31, 2022 at 07:59AM: How can I correspond a hypothesis to a decidable axiom in match (in Coq)? – proofassistants.stackexchange.com
StackExchange Bot (Aug 31 2022 at 14:44):Andrey posted a new question on August 31, 2022 at 04:07PM: I'm trying to build a proof in Coq that two different permutation definitions are equivalent, but the non-inductive side is not working – stackoverflow.com
StackExchange Bot (Sep 01 2022 at 05:44):with-forest posted a new question on September 01, 2022 at 06:35AM: Can I unfold not all things but only one thing in Coq? – proofassistants.stackexchange.com
StackExchange Bot (Sep 02 2022 at 03:44):with-forest posted a new question on September 02, 2022 at 04:12AM: If I make some new structure like Q, then can I use 'rewrite' tactic for my new structure in Coq? – proofassistants.stackexchange.com
StackExchange Bot (Sep 02 2022 at 16:45):op325 posted a new question on September 02, 2022 at 05:59PM: setoid_rewrite failed with MathClasses Coq – stackoverflow.com
StackExchange Bot (Sep 08 2022 at 12:44):Bodo posted a new question on September 08, 2022 at 02:18PM: Overloading operators in Coq via typeclasses and notation scopes: Is there anything special about the '+' and '*' symbols? – stackoverflow.com
StackExchange Bot (Sep 11 2022 at 10:44):nicolas posted a new question on September 11, 2022 at 12:09PM: Using proof assistants to generate fast code – proofassistants.stackexchange.com
StackExchange Bot (Sep 15 2022 at 16:44):Rincewind posted a new question on September 15, 2022 at 05:23PM: .CoqMakefile.d required by CoqMakefile but not generated – proofassistants.stackexchange.com
StackExchange Bot (Sep 18 2022 at 13:44):Taimoor Zaeem posted a new question on September 18, 2022 at 03:34PM: How do I exit coqtop REPL? – stackoverflow.com
StackExchange Bot (Sep 19 2022 at 07:44):silver-ymz posted a new question on September 19, 2022 at 09:17AM: Can someone help me with this proof about the pumping lemma using coq? – stackoverflow.com
StackExchange Bot (Sep 27 2022 at 22:44):sudgy posted a new question on September 28, 2022 at 12:35AM: Coq Typeclass on Functions Gets Confused by Equality – proofassistants.stackexchange.com
StackExchange Bot (Sep 28 2022 at 09:44):rsaill posted a new question on September 28, 2022 at 10:54AM: Using VST with GCC – stackoverflow.com
StackExchange Bot (Sep 29 2022 at 04:44):Yu-Fang Chen posted a new question on September 29, 2022 at 06:05AM: Install why3-coq on MacBook Pro – stackoverflow.com
StackExchange Bot (Oct 04 2022 at 17:44):bruhhbruh posted a new question on October 04, 2022 at 07:39PM: How to convince coq that if (a * c) = (b * c), and c is not equal to 0, then a=b – stackoverflow.com
StackExchange Bot (Oct 05 2022 at 13:44):KingsAlpaca posted a new question on October 05, 2022 at 03:36PM: How to rearrange newly defined associative terms in Coq? – stackoverflow.com
StackExchange Bot (Oct 13 2022 at 01:44):Zak Kent posted a new question on October 13, 2022 at 03:03AM: Default Implementation of Coq typeclass methods – stackoverflow.com
StackExchange Bot (Oct 14 2022 at 16:44):Stefan posted a new question on October 14, 2022 at 06:32PM: Proof of "less than or equal" transitive law in Coq – stackoverflow.com
StackExchange Bot (Oct 15 2022 at 02:44):Huan Sun posted a new question on October 15, 2022 at 03:53AM: concurrent separation logic in Isabelle – stackoverflow.com
StackExchange Bot (Oct 15 2022 at 10:44):Stefan posted a new question on October 15, 2022 at 12:20PM: Proof that "if m <= n then max(m, n) = n" in Coq – stackoverflow.com
StackExchange Bot (Oct 19 2022 at 15:44):sp1ff posted a new question on October 19, 2022 at 04:19PM: How to scope Search to the current module only – stackoverflow.com
StackExchange Bot (Oct 19 2022 at 22:44):mateus filipe posted a new question on October 19, 2022 at 11:10PM: prove DeMorgan law in coq – stackoverflow.com
StackExchange Bot (Oct 20 2022 at 08:44):Dave posted a new question on October 20, 2022 at 10:37AM: Universe polymorphism and modules in Coq – proofassistants.stackexchange.com
StackExchange Bot (Oct 20 2022 at 18:44):TonyBlabla posted a new question on October 20, 2022 at 08:06PM: Prove that if a <= b, then max ( a , b ) = b in Coq – stackoverflow.com
StackExchange Bot (Oct 26 2022 at 20:44):Alessandro D'angelo posted a new question on October 26, 2022 at 09:37PM: Proving theorem in Coq, the number of occurances in a list is <= the lenght of this list – stackoverflow.com
StackExchange Bot (Oct 27 2022 at 00:44):Alessandro D'angelo posted a new question on October 27, 2022 at 01:04AM: Prove that the number of occurences of x in a list that has n position with valor x = n – stackoverflow.com
StackExchange Bot (Nov 03 2022 at 04:44):Bennett Kahn posted a new question on November 03, 2022 at 04:54AM: How do I work with ints when using coq-of-ocaml for OCaml to Coq conversion? – proofassistants.stackexchange.com
StackExchange Bot (Nov 04 2022 at 15:44):임기정 posted a new question on November 04, 2022 at 03:16PM: To prove the unfolding lemma for some – stackoverflow.com
StackExchange Bot (Nov 05 2022 at 18:44):Kamyar Mirzavaziri posted a new question on November 05, 2022 at 06:31PM: Definition by minimization in Coq – stackoverflow.com
StackExchange Bot (Nov 08 2022 at 13:44):op325 posted a new question on November 08, 2022 at 01:04PM: Coq ssreflect - rewrite inside \big – proofassistants.stackexchange.com
StackExchange Bot (Nov 09 2022 at 01:44):dganti posted a new question on November 09, 2022 at 02:02AM: COQ returns cannot guess decreasing argument of fix. How to fix my function? – stackoverflow.com
Notification Bot (Nov 09 2022 at 09:46):A message was moved from this topic to #VsCoq devs & users > VsCoq error by Karl Palmskog.
StackExchange Bot (Nov 10 2022 at 09:44):acid posted a new question on November 10, 2022 at 08:45AM: How can I write a proof to match inductive type without using forall in its subterm? – stackoverflow.com
StackExchange Bot (Nov 11 2022 at 06:44):Charlie Parker posted a new question on November 11, 2022 at 06:30AM: How does one translate Lean to Coq (and visa versa)? – proofassistants.stackexchange.com
StackExchange Bot (Nov 16 2022 at 04:44):Nathan posted a new question on November 16, 2022 at 04:08AM: Why are these two proofs so different? – proofassistants.stackexchange.com
StackExchange Bot (Nov 17 2022 at 09:44):Åsmund Kløvstad posted a new question on November 17, 2022 at 10:08AM: Applying custom tactic in hypothesis – proofassistants.stackexchange.com
StackExchange Bot (Nov 19 2022 at 09:44):ZhangLiao posted a new question on November 19, 2022 at 10:15AM: Pirnting Coq definition without loading library – stackoverflow.com
StackExchange Bot (Nov 19 2022 at 22:44):ZhangLiao posted a new question on November 19, 2022 at 10:15AM: Printing Coq definition without loading library – stackoverflow.com
StackExchange Bot (Nov 20 2022 at 13:44):Moti posted a new question on November 20, 2022 at 01:58PM: Cannot open pixbuf loader module file in Windows – proofassistants.stackexchange.com
StackExchange Bot (Nov 20 2022 at 13:44):ch271828n posted a new question on November 20, 2022 at 02:13PM: Is it possible to convert all higher-order logic and dependent type in Lean/Isabelle/Coq into first-order logic? – stackoverflow.com
StackExchange Bot (Nov 24 2022 at 00:44):Bromind posted a new question on November 24, 2022 at 12:17AM: Proving Union of Ensemble is not Empty_set – stackoverflow.com
StackExchange Bot (Nov 24 2022 at 20:44):TonyBlabla posted a new question on November 24, 2022 at 08:29PM: Big Step Substraction – stackoverflow.com
StackExchange Bot (Nov 25 2022 at 07:44):user20531868 posted a new question on November 25, 2022 at 07:02AM: Question about failure to match wildcard character "_" – stackoverflow.com
StackExchange Bot (Nov 25 2022 at 16:44):ax_fer posted a new question on November 25, 2022 at 04:04PM: Verified software toolchain : which tactic to apply commutativity in mpred – stackoverflow.com
StackExchange Bot (Nov 29 2022 at 05:44):Huan Sun posted a new question on November 29, 2022 at 05:19AM: type variable in datatype definition – stackoverflow.com
StackExchange Bot (Dec 06 2022 at 11:46):xmepl posted a new question on December 06, 2022 at 12:00PM: Coq Problem where i dont know how to continue – stackoverflow.com
StackExchange Bot (Dec 07 2022 at 08:45):user1901 posted a new question on December 07, 2022 at 08:43AM: How do I prove a record related lemma? – proofassistants.stackexchange.com
StackExchange Bot (Dec 10 2022 at 22:45):Charlie Parker posted a new question on December 10, 2022 at 09:56PM: How does one install a opam coq package that has been successfully install previously? – stackoverflow.com
StackExchange Bot (Dec 10 2022 at 23:45):Charlie Parker posted a new question on December 10, 2022 at 11:53PM: How to install the coq 8.14 package with opam pin when it says it can't find it? – stackoverflow.com
StackExchange Bot (Dec 11 2022 at 03:45):Charlie Parker posted a new question on December 10, 2022 at 11:53PM: How to install the coq 8.14 (or 8.15) package with opam pin when it says it can't find it? – stackoverflow.com
StackExchange Bot (Dec 11 2022 at 23:46):Charlie Parker posted a new question on December 12, 2022 at 12:36AM: How does one print proof terms as de bruijn indices instead of random named variables in Coq? – stackoverflow.com
StackExchange Bot (Dec 12 2022 at 10:44):pjm posted a new question on December 12, 2022 at 11:24AM: Coq: Unification fails with record – stackoverflow.com
StackExchange Bot (Dec 13 2022 at 13:49):Huan Sun posted a new question on December 13, 2022 at 02:00PM: What does InjL and InjR operator means in coq-Iris? – stackoverflow.com
StackExchange Bot (Dec 18 2022 at 02:45):Joshua Meyers posted a new question on December 18, 2022 at 03:04AM: How can I hide all proof terms? – stackoverflow.com
StackExchange Bot (Dec 18 2022 at 19:48):limitedeternity posted a new question on December 18, 2022 at 07:48PM: Proving theorems containing bitwise operators – stackoverflow.com
StackExchange Bot (Dec 19 2022 at 23:48):Arnie2C_A posted a new question on December 20, 2022 at 12:35AM: How to avoid "Cannot guess decreasing argument of fix." in Coq – stackoverflow.com
StackExchange Bot (Dec 21 2022 at 15:48):Jesper posted a new question on December 21, 2022 at 03:51PM: What was the first proof assistant with eta equality for records? – proofassistants.stackexchange.com
StackExchange Bot (Dec 23 2022 at 15:44):Arnie2C_A posted a new question on December 23, 2022 at 04:06PM: Two Coq Problems SOS: one is about IndProp, another has something to do with recursion, I guess – stackoverflow.com
StackExchange Bot (Dec 24 2022 at 08:44):コンピューターバカ posted a new question on December 24, 2022 at 09:15AM: induction integer record in coq – stackoverflow.com
StackExchange Bot (Dec 25 2022 at 05:44):scubed posted a new question on December 25, 2022 at 06:42AM: Rewrite with variable from inner scope? – stackoverflow.com
StackExchange Bot (Dec 25 2022 at 05:44):scubed posted a new question on December 25, 2022 at 06:43AM: Fix vs. Fix_sub – stackoverflow.com
StackExchange Bot (Dec 25 2022 at 18:44):Charles Averill posted a new question on December 25, 2022 at 07:42PM: How do I approach the final inductive step in plus_leb_compat_l from Software Foundations? – proofassistants.stackexchange.com
StackExchange Bot (Dec 31 2022 at 05:44):Charles Averill posted a new question on December 31, 2022 at 04:51AM: How do I approach the final step in proving the cancellation law in Coq? – proofassistants.stackexchange.com
StackExchange Bot (Jan 01 2023 at 19:44):Charles Averill posted a new question on January 01, 2023 at 08:34PM: Do you need to pass in template types to functions that accept template objects in Coq? – stackoverflow.com
StackExchange Bot (Jan 04 2023 at 07:44):scubed posted a new question on January 04, 2023 at 07:45AM: Is it possible to destruct and rewrite simultaneously? – stackoverflow.com
StackExchange Bot (Jan 06 2023 at 03:44):Travis Allison posted a new question on January 06, 2023 at 04:12AM: Exhaustiveness matching in proof objects for induction in Coq – stackoverflow.com
StackExchange Bot (Jan 07 2023 at 16:44):Ícaro Lorran posted a new question on January 07, 2023 at 04:55PM: How do I write a summation on Coq? – cstheory.stackexchange.com
StackExchange Bot (Jan 07 2023 at 18:44):Pietro Braione posted a new question on January 07, 2023 at 07:37PM: How do I define a function in Coq with if...then..else behavior? – proofassistants.stackexchange.com
StackExchange Bot (Jan 07 2023 at 21:45):Ben Little posted a new question on January 07, 2023 at 10:39PM: How to convert hypothesis with "if then else" equality into its consequent using coq? – proofassistants.stackexchange.com
StackExchange Bot (Jan 08 2023 at 17:44):Ícaro Lorran posted a new question on January 08, 2023 at 05:13PM: How to write a summation in Coq – proofassistants.stackexchange.com
StackExchange Bot (Jan 13 2023 at 03:44):hilberts_drinking_problem posted a new question on January 13, 2023 at 03:27AM: Subsequences in Coq – proofassistants.stackexchange.com
StackExchange Bot (Jan 14 2023 at 22:44):Ben Little posted a new question on January 14, 2023 at 10:50PM: Are there any ergonomic ways to deal with finite types in Coq? – proofassistants.stackexchange.com
StackExchange Bot (Jan 19 2023 at 22:47):amit9oct posted a new question on January 19, 2023 at 10:55PM: Imports in multi-file Coq projects – stackoverflow.com
StackExchange Bot (Jan 20 2023 at 22:45):Agnishom Chattopadhyay posted a new question on January 20, 2023 at 11:20PM: Coq simpl failing to do beta reduction in this double fixpoint expression – proofassistants.stackexchange.com
StackExchange Bot (Jan 21 2023 at 03:44):Andre posted a new question on January 21, 2023 at 04:24AM: Vacuously true implications in Coq – stackoverflow.com
StackExchange Bot (Jan 21 2023 at 19:45):Agnishom Chattopadhyay posted a new question on January 20, 2023 at 11:20PM: Coq simpl failing to do beta reduction in this fixpoint expression – proofassistants.stackexchange.com
StackExchange Bot (Jan 23 2023 at 18:46):dvr posted a new question on January 23, 2023 at 07:19PM: using addf_div for rat_numDomainType – stackoverflow.com
StackExchange Bot (Jan 23 2023 at 23:44):dvr posted a new question on January 23, 2023 at 11:13PM: Understanding \is a unit in ssreflect – stackoverflow.com
StackExchange Bot (Jan 24 2023 at 20:46):markasoftware posted a new question on January 24, 2023 at 09:16PM: In Coq, why is nat a Type, even though it's actually a Set? – stackoverflow.com
StackExchange Bot (Jan 24 2023 at 22:47):Agnishom Chattopadhyay posted a new question on January 24, 2023 at 10:41PM: In Coq, is there a simpler tactic for introducing a disjunction and immediately destructing it? – proofassistants.stackexchange.com
StackExchange Bot (Jan 26 2023 at 00:49):user2506946 posted a new question on January 26, 2023 at 01:42AM: Beta expansion in coq: can I make a term into a function, abstracting over another given term? – stackoverflow.com
StackExchange Bot (Jan 28 2023 at 16:45):FH35 posted a new question on January 28, 2023 at 05:29PM: Is it possible to make Coq accept a class of Fixpoint functions if we provide proofs of argument size reduction? – stackoverflow.com
StackExchange Bot (Jan 28 2023 at 22:45):nobody posted a new question on January 28, 2023 at 11:34PM: Forcing evaluation of terms before extraction, or other ways to test extracted functions? – stackoverflow.com
StackExchange Bot (Jan 29 2023 at 20:44):Lomega posted a new question on January 29, 2023 at 09:20PM: "Cannot instantiate metavariable P of type ..." when destructing in Coq proof mode – stackoverflow.com
StackExchange Bot (Jan 30 2023 at 22:03):Adrian L posted a new question on January 30, 2023 at 10:08PM: Destruction of bound dependent types – proofassistants.stackexchange.com
StackExchange Bot (Jan 31 2023 at 20:46):Arjun Viswanathan posted a new question on January 31, 2023 at 09:18PM: Is there a way to redirect Coqide messages and errors to the same output? – stackoverflow.com
StackExchange Bot (Feb 01 2023 at 21:46):Pietro Braione posted a new question on February 01, 2023 at 09:19PM: What is the idiomatic way in Coq to write recursive functions over product types? – proofassistants.stackexchange.com
StackExchange Bot (Feb 02 2023 at 15:47):Pietro Braione posted a new question on February 02, 2023 at 04:27PM: How do I express a fixpoint of a decreasing argument that is not a subterm of the function's argument? – proofassistants.stackexchange.com
StackExchange Bot (Feb 03 2023 at 08:44):FH35 posted a new question on February 03, 2023 at 09:16AM: Another question about how to make Coq accept a Fixpoint definition – stackoverflow.com
StackExchange Bot (Feb 07 2023 at 07:44):greg. posted a new question on February 07, 2023 at 07:20AM: Lean4: Proving that (xs = ys) = (reverse xs = reverse ys) – stackoverflow.com
StackExchange Bot (Feb 08 2023 at 09:44):footnotes posted a new question on February 08, 2023 at 10:23AM: How to prove A \/ False -> A in Coq? – stackoverflow.com
StackExchange Bot (Feb 08 2023 at 18:44):larsr posted a new question on February 08, 2023 at 06:38PM: How does one expand a fix function just one step? – stackoverflow.com
StackExchange Bot (Feb 10 2023 at 18:44):matteo_c posted a new question on February 10, 2023 at 06:56PM: Stream of all finite prefixes of a stream – proofassistants.stackexchange.com
StackExchange Bot (Feb 11 2023 at 03:44):sdpoll posted a new question on February 11, 2023 at 03:47AM: Why can't I write a function that doesn't take a type argument besides Set, Prop, or Type? – proofassistants.stackexchange.com
StackExchange Bot (Feb 12 2023 at 11:44):Bruno posted a new question on February 10, 2023 at 11:07AM: Why does Ltac not match the clause? – stackoverflow.com
StackExchange Bot (Feb 13 2023 at 17:44):matteo_c posted a new question on February 13, 2023 at 06:23PM: Two-step induction of inductive predicate on Streams – proofassistants.stackexchange.com
StackExchange Bot (Feb 13 2023 at 21:44):Zazaeil posted a new question on February 13, 2023 at 10:39PM: Does ∃! x, ∃! y, P (x, y) imply ∃! xy, P (fst xy) (snd xy)? – stackoverflow.com
StackExchange Bot (Feb 14 2023 at 00:44):Charlie Parker posted a new question on February 13, 2023 at 11:51PM: How does one make sure that coq project installed correctly when it doesn't seem to appear on opam list? – stackoverflow.com
StackExchange Bot (Feb 14 2023 at 18:44):Charlie Parker posted a new question on February 14, 2023 at 07:42PM: How do I install ocamlfind first properly before other opam packages without root permissions? – stackoverflow.com
StackExchange Bot (Feb 14 2023 at 20:44):Charlie Parker posted a new question on February 14, 2023 at 08:22PM: How does one pin/freeze a version of the dependencies of an opam project/package and then install the project with such specified dependencies? – stackoverflow.com
StackExchange Bot (Feb 15 2023 at 19:44):Charlie Parker posted a new question on February 15, 2023 at 08:32PM: How does one install coq-serapi for coq 8.10 using opam pin and ideally using a commit from coq-serapi? – stackoverflow.com
StackExchange Bot (Feb 15 2023 at 21:44):Charlie Parker posted a new question on February 15, 2023 at 09:49PM: What is the tag for menhir for coq 8.12 when installing it with opam install -y? – stackoverflow.com
StackExchange Bot (Feb 15 2023 at 23:44):massive coq posted a new question on February 15, 2023 at 11:49PM: Coq abilities and usage – proofassistants.stackexchange.com
StackExchange Bot (Feb 16 2023 at 14:44):M B posted a new question on February 16, 2023 at 03:16PM: How to get rid of opaque proof-terms in computation – proofassistants.stackexchange.com
StackExchange Bot (Feb 17 2023 at 18:44):Lomega posted a new question on February 17, 2023 at 06:22PM: Fail to destruct due to ill-typedness and even cannot give an exact term in Coq – stackoverflow.com
StackExchange Bot (Feb 17 2023 at 21:44):user2506946 posted a new question on February 17, 2023 at 09:58PM: How to overload the "+" notation in Coq? – stackoverflow.com
StackExchange Bot (Feb 22 2023 at 23:03):David Monniaux posted a new question on February 22, 2023 at 11:29PM: an argument why stack blocks are never unexpectedly freed in the RTL intermediate language in CompCert – proofassistants.stackexchange.com
StackExchange Bot (Feb 23 2023 at 15:44):M B posted a new question on February 23, 2023 at 04:34PM: Program Fixpoint decreasing on measure produces unsolvable goal – proofassistants.stackexchange.com
StackExchange Bot (Feb 23 2023 at 17:44):Coqerellen posted a new question on February 23, 2023 at 05:32PM: Destructing transitivity hypothesis on simple predicate logic – proofassistants.stackexchange.com
StackExchange Bot (Mar 05 2023 at 00:44):markasoftware posted a new question on March 05, 2023 at 12:10AM: How to break up an implication into two subgoals in Coq? – stackoverflow.com
StackExchange Bot (Mar 07 2023 at 15:44):asha soroushpoor posted a new question on March 07, 2023 at 03:39PM: Coq Induction on Hypothesis destroys the Hypothesis – proofassistants.stackexchange.com
StackExchange Bot (Mar 10 2023 at 19:44):Zazaeil posted a new question on March 10, 2023 at 07:02PM: Yet another constructive (Coq) proof that nat -> nat -> nat is not bijective. How to explain it to myself? – cstheory.stackexchange.com
StackExchange Bot (Mar 11 2023 at 10:44):user65526 posted a new question on March 11, 2023 at 10:45AM: Understanding a message on CoqIde – stackoverflow.com
StackExchange Bot (Mar 11 2023 at 12:44):user65526 posted a new question on March 11, 2023 at 01:22PM: Complete Atomic Boolean algebras in Coq – stackoverflow.com
StackExchange Bot (Mar 11 2023 at 14:44):user65526 posted a new question on March 11, 2023 at 02:53PM: Activating nested proof – stackoverflow.com
StackExchange Bot (Mar 11 2023 at 18:44):user65526 posted a new question on March 11, 2023 at 05:49PM: Definite description operator in Coq – stackoverflow.com
StackExchange Bot (Mar 14 2023 at 08:44):8bc3 457f posted a new question on March 14, 2023 at 09:35AM: How to abstract over function arity in Lean and Coq? – proofassistants.stackexchange.com
StackExchange Bot (Mar 14 2023 at 11:44):user65526 posted a new question on March 14, 2023 at 11:42AM: Unclear error message regarding format and notation – stackoverflow.com
StackExchange Bot (Mar 14 2023 at 16:44):anonymous12345677654 posted a new question on March 14, 2023 at 04:45PM: How can I write a filter function for sequences represented as functions in Coq? – stackoverflow.com
StackExchange Bot (Mar 15 2023 at 15:44):radrow posted a new question on March 15, 2023 at 04:20PM: How to create a custom Ltac to recursively destruct conjunctions? – stackoverflow.com
StackExchange Bot (Mar 20 2023 at 12:44):user65526 posted a new question on March 20, 2023 at 01:20PM: Disjunction and the error `No product after head reduction' – stackoverflow.com
StackExchange Bot (Mar 20 2023 at 18:44):Felipe posted a new question on March 20, 2023 at 06:14PM: How to reason about equality between different datatypes? – proofassistants.stackexchange.com
StackExchange Bot (Mar 20 2023 at 21:44):Yousef Alhessi posted a new question on March 20, 2023 at 09:53PM: Proving n + S n = S (n + n) without n + S m = S (n + m) – stackoverflow.com
StackExchange Bot (Mar 21 2023 at 06:44):Raul Gomez posted a new question on March 21, 2023 at 07:32AM: I don't know how to fire up coqtail – proofassistants.stackexchange.com
StackExchange Bot (Mar 21 2023 at 08:44):Lepticed posted a new question on March 21, 2023 at 09:19AM: How to distribute an AND operator in Coq? – stackoverflow.com
StackExchange Bot (Mar 21 2023 at 16:44):user65526 posted a new question on March 21, 2023 at 04:39PM: A proof by cases – stackoverflow.com
StackExchange Bot (Mar 21 2023 at 17:44):user65526 posted a new question on March 21, 2023 at 04:39PM: The apply rule in proof by cases – stackoverflow.com
StackExchange Bot (Mar 22 2023 at 11:44):anurag posted a new question on March 22, 2023 at 11:59AM: How to formally verify a compiler (frontend and/or backend)? – stackoverflow.com
StackExchange Bot (Mar 22 2023 at 11:44):user65526 posted a new question on March 22, 2023 at 12:12PM: Why do these theorems of propositional logic allow for the same proof in Coq? – stackoverflow.com
StackExchange Bot (Mar 23 2023 at 04:44):sudgy posted a new question on March 23, 2023 at 04:24AM: Rewrite with definitional equality and dependent types – proofassistants.stackexchange.com
StackExchange Bot (Mar 23 2023 at 08:44):コンピューターバカ posted a new question on March 23, 2023 at 08:35AM: How to use induction tactic on recursively defined functions in Coq – stackoverflow.com
StackExchange Bot (Mar 24 2023 at 01:44):コンピューターバカ posted a new question on March 23, 2023 at 08:35AM: How to proof recursively defined functions' prop in Coq – stackoverflow.com
StackExchange Bot (Mar 25 2023 at 13:44):anonymous12345677654 posted a new question on March 25, 2023 at 02:39PM: What is a way to represent non-disjoint union in Coq? – stackoverflow.com
StackExchange Bot (Mar 25 2023 at 18:44):Mohan Radhakrishnan posted a new question on March 25, 2023 at 06:31PM: 'coqc' does not find findlib.conf – stackoverflow.com
StackExchange Bot (Mar 30 2023 at 10:44):Lepticed posted a new question on March 30, 2023 at 12:06PM: How can I better structure Coq files? – stackoverflow.com
StackExchange Bot (Mar 30 2023 at 11:44):Lepticed posted a new question on March 30, 2023 at 01:31PM: How to deal with lemma only used once in Coq? – stackoverflow.com
StackExchange Bot (Mar 31 2023 at 14:44):pjm posted a new question on March 31, 2023 at 02:54PM: Morphism signature for dependently-typed vectors in coq – stackoverflow.com
StackExchange Bot (Apr 01 2023 at 00:44):Lepticed posted a new question on April 01, 2023 at 01:32AM: How to write the iota descriptor in Coq? – stackoverflow.com
StackExchange Bot (Apr 02 2023 at 20:44):Agnishom Chattopadhyay posted a new question on April 02, 2023 at 09:08PM: Why can't I use let bindings to pattern match a 3-tuple in Coq? – proofassistants.stackexchange.com
StackExchange Bot (Apr 04 2023 at 05:44):Alex Byard posted a new question on April 04, 2023 at 07:34AM: How do different dependently typed languages compare with one another? – proofassistants.stackexchange.com
StackExchange Bot (Apr 05 2023 at 14:01):kbridge4096 posted a new question on April 05, 2023 at 02:09PM: Model and Prove Unsigned Integer Operation Wrapping Behavior in Coq – proofassistants.stackexchange.com
StackExchange Bot (Apr 05 2023 at 16:16):Lepticed posted a new question on April 05, 2023 at 05:09PM: Use the contrapositive of an hypothesis in Coq – stackoverflow.com
StackExchange Bot (Apr 12 2023 at 01:46):Randomuser6781 posted a new question on April 12, 2023 at 03:01AM: How do I prove this theorem with induction in COQ – proofassistants.stackexchange.com
StackExchange Bot (Apr 12 2023 at 03:44):anonymouse 29083 posted a new question on April 12, 2023 at 04:03AM: Help solve these proofs – proofassistants.stackexchange.com
StackExchange Bot (Apr 12 2023 at 08:45):hch posted a new question on April 12, 2023 at 09:01AM: stuck trying to prove sublist of list – proofassistants.stackexchange.com
StackExchange Bot (Apr 12 2023 at 08:45):hch posted a new question on April 12, 2023 at 09:16AM: stuck trying to prove sublist of list – stackoverflow.com
StackExchange Bot (Apr 12 2023 at 12:46):HELLOBIRD 892 posted a new question on April 12, 2023 at 04:03AM: nvmnvmnvmnvmnvmnvmnvmnvmnvmnvmnvmnvm – proofassistants.stackexchange.com
StackExchange Bot (Apr 13 2023 at 11:48):anonymous12345677654 posted a new question on April 13, 2023 at 12:36PM: Is there a library for sets that works with bool in Coq? – stackoverflow.com
StackExchange Bot (Apr 14 2023 at 07:44):bodacious_bandit posted a new question on April 14, 2023 at 08:51AM: How do I prove an expression in Coq that involves pattern matching? – proofassistants.stackexchange.com
StackExchange Bot (Apr 14 2023 at 09:44):Sebastian Graf posted a new question on April 14, 2023 at 10:51AM: Is there a formalism of "coinductive" data types with negative occurrences? – proofassistants.stackexchange.com
StackExchange Bot (Apr 14 2023 at 12:44):Bob posted a new question on April 14, 2023 at 01:58PM: How to use the pretty-printer of CompCert in the OCaml toplevel? – stackoverflow.com
StackExchange Bot (Apr 15 2023 at 02:44):bodacious_bandit posted a new question on April 15, 2023 at 03:47AM: How do I prove this property about a factorial specification in Coq? – proofassistants.stackexchange.com
StackExchange Bot (Apr 17 2023 at 00:44):Agnishom Chattopadhyay posted a new question on April 17, 2023 at 02:43AM: How to prove this correctness principle of transposition of lists of lists in Coq? – proofassistants.stackexchange.com
StackExchange Bot (Apr 17 2023 at 15:45):rex posted a new question on April 17, 2023 at 05:39PM: How to parse a string into a list of lists in Coq? – stackoverflow.com
StackExchange Bot (Apr 18 2023 at 03:44):randompss posted a new question on April 18, 2023 at 05:21AM: Trying to solve this proof using the induction theorem but I am stuck – proofassistants.stackexchange.com
StackExchange Bot (Apr 19 2023 at 22:45):user12456500 posted a new question on April 19, 2023 at 11:56PM: Syntax error: '.' expected after [vernac:gallina] (in [vernac_aux]) in Coq when using inductive with integers – stackoverflow.com
StackExchange Bot (Apr 20 2023 at 14:46):anonymous12345677654 posted a new question on April 20, 2023 at 04:03PM: Type coercions in finset – stackoverflow.com
StackExchange Bot (Apr 21 2023 at 14:46):Felipe posted a new question on April 21, 2023 at 03:42PM: Rewriting with heterogeneous equality (JMeq) – proofassistants.stackexchange.com
StackExchange Bot (Apr 22 2023 at 00:44):Pavel Shuhray posted a new question on April 22, 2023 at 02:34AM: Dependent sum and equality with Coq – proofassistants.stackexchange.com
StackExchange Bot (Apr 24 2023 at 18:46):nobody posted a new question on April 24, 2023 at 06:58PM: fresh name: use match result if variable, do something else if it's a constant – stackoverflow.com
StackExchange Bot (Apr 25 2023 at 03:44):itsFrank posted a new question on April 25, 2023 at 05:34AM: How to solve this proof – proofassistants.stackexchange.com
StackExchange Bot (Apr 25 2023 at 06:44):itsFrank posted a new question on April 25, 2023 at 05:34AM: Hwo to prove basic lemmas about divisibility in Coq? – proofassistants.stackexchange.com
StackExchange Bot (Apr 26 2023 at 06:44):aaay posted a new question on April 26, 2023 at 08:17AM: Recursion and Pattern matching in Coq – stackoverflow.com
StackExchange Bot (Apr 27 2023 at 10:44):Bas Laarakker posted a new question on April 27, 2023 at 11:15AM: Can I show Coq equality of types without using a mapping between the types? – proofassistants.stackexchange.com
StackExchange Bot (Apr 27 2023 at 15:45):itsFrank posted a new question on April 25, 2023 at 05:34AM: How to prove basic lemmas about divisibility in Coq? – proofassistants.stackexchange.com
StackExchange Bot (Apr 28 2023 at 01:45):Qinshi Wang posted a new question on April 28, 2023 at 03:05AM: Coq: Unify with a pattern and get the result – proofassistants.stackexchange.com
StackExchange Bot (Apr 30 2023 at 07:45):8bc3 457f posted a new question on April 30, 2023 at 08:13AM: Inductive vs. recursive definitions – proofassistants.stackexchange.com
StackExchange Bot (Apr 30 2023 at 07:45):8bc3 457f posted a new question on April 30, 2023 at 08:22AM: Debug autorewrite in Coq – proofassistants.stackexchange.com
StackExchange Bot (May 01 2023 at 05:45):sudgy posted a new question on May 01, 2023 at 07:05AM: Weird use of equality in Coq – proofassistants.stackexchange.com
StackExchange Bot (May 01 2023 at 14:46):Tony Peterson posted a new question on May 01, 2023 at 04:12PM: Coq: Proving snd divmod doesn't depend on parameter q? – proofassistants.stackexchange.com
StackExchange Bot (May 02 2023 at 20:56):Alexandr posted a new question on May 02, 2023 at 10:09PM: How to proof this "Theorem spec0 : forall m n p k, (p <= k) -> (p | n) -> (p | m) -> p <= help m n k." in coq? – stackoverflow.com
StackExchange Bot (May 02 2023 at 22:05):dvr posted a new question on May 02, 2023 at 11:22PM: Raising a natural number, int, or rat to a rational? – stackoverflow.com
StackExchange Bot (May 03 2023 at 12:44):Felipe posted a new question on May 03, 2023 at 01:44PM: Reasoning about non reflexive equalities & type conversions – proofassistants.stackexchange.com
StackExchange Bot (May 05 2023 at 20:45):user21829651 posted a new question on May 05, 2023 at 10:08PM: Software Foundations Basics Exercise - How do I access letter from grade? – stackoverflow.com
StackExchange Bot (May 07 2023 at 10:44):Jay Lee posted a new question on May 07, 2023 at 12:10PM: Ltac tactic that accepts an arbitrary number of quantifiers – stackoverflow.com
StackExchange Bot (May 09 2023 at 12:45):Bas Laarakker posted a new question on May 09, 2023 at 01:07PM: Rewriting within sigma types in Coq – stackoverflow.com
StackExchange Bot (May 10 2023 at 18:45):Agnishom Chattopadhyay posted a new question on May 10, 2023 at 06:53PM: How to deduce this equality based on the fact that these two terms must be the same? – proofassistants.stackexchange.com
StackExchange Bot (May 11 2023 at 10:46):dvr posted a new question on May 11, 2023 at 12:25PM: Coerce rat to realType im math-comp/analysis – stackoverflow.com
StackExchange Bot (May 11 2023 at 21:44):Felipe Morelli posted a new question on May 11, 2023 at 10:01PM: Help with proofs in analysis – proofassistants.stackexchange.com
StackExchange Bot (May 13 2023 at 09:44):Henri_S posted a new question on May 13, 2023 at 10:45AM: Can I define nested mutually dependent types in Coq? – cstheory.stackexchange.com
StackExchange Bot (May 13 2023 at 21:45):Jack posted a new question on May 13, 2023 at 11:42PM: Proof List Inequality in Coq – cstheory.stackexchange.com
StackExchange Bot (May 14 2023 at 10:44):with-forest posted a new question on May 14, 2023 at 11:03AM: Is it possible to make a proof assistant program based on ZFC? – proofassistants.stackexchange.com
StackExchange Bot (May 15 2023 at 12:45):shooqie posted a new question on May 15, 2023 at 02:32PM: Non-trivial Fixpoint on nested recursive types – stackoverflow.com
StackExchange Bot (May 15 2023 at 13:45):Tilman Zuckmantel posted a new question on May 15, 2023 at 03:34PM: Importing a Module in Coq – stackoverflow.com
StackExchange Bot (May 15 2023 at 19:45):Jeff Witnick posted a new question on May 15, 2023 at 08:23PM: Induction COQ Question – proofassistants.stackexchange.com
StackExchange Bot (May 15 2023 at 19:45):Jeff Witnick posted a new question on May 15, 2023 at 09:34PM: Help I am confused...Proof Assistant – proofassistants.stackexchange.com
StackExchange Bot (May 15 2023 at 22:45):Jeff Witnick posted a new question on May 16, 2023 at 12:42AM: Equivalence Relations COQ – proofassistants.stackexchange.com
StackExchange Bot (May 16 2023 at 00:44):Jeff Witnick posted a new question on May 16, 2023 at 02:21AM: Help with strong induction – proofassistants.stackexchange.com
StackExchange Bot (May 16 2023 at 12:45):Jeff Witnick posted a new question on May 16, 2023 at 02:33PM: Help with Divisibility and GCD – proofassistants.stackexchange.com
StackExchange Bot (May 16 2023 at 18:45):deleted_user0972 posted a new question on May 15, 2023 at 08:23PM: inductive COQ concern – proofassistants.stackexchange.com
StackExchange Bot (May 16 2023 at 18:45):randomguest0002 posted a new question on May 16, 2023 at 08:44PM: coq proof question – proofassistants.stackexchange.com
StackExchange Bot (May 17 2023 at 04:44):randomguest0002 posted a new question on May 16, 2023 at 08:44PM: Organizing a Coq proof – proofassistants.stackexchange.com
StackExchange Bot (May 17 2023 at 17:44):deleted_user0972 posted a new question on May 15, 2023 at 09:34PM: No subterm matching Hab * a – proofassistants.stackexchange.com
StackExchange Bot (May 19 2023 at 20:45):Tilman Zuckmantel posted a new question on May 19, 2023 at 10:39PM: How to use a constructor within its own inductive definition in Coq (circular dependencies)? – stackoverflow.com
StackExchange Bot (May 20 2023 at 12:44):Tilman Zuckmantel posted a new question on May 20, 2023 at 01:44PM: How to use a proof about a datatype within the same datatype definition in Coq? – stackoverflow.com
StackExchange Bot (May 20 2023 at 19:45):epelaez posted a new question on May 20, 2023 at 09:20PM: Replace element in Coq list – stackoverflow.com
StackExchange Bot (May 23 2023 at 22:44):D Left Adjoint to U posted a new question on May 24, 2023 at 12:02AM: Can Coq grab some data over HTTP and then write the data as declartions in Coq itself? – proofassistants.stackexchange.com
StackExchange Bot (May 27 2023 at 20:44):Hank Lenzi posted a new question on May 27, 2023 at 09:07PM: Dummett's view on L.E.M. in Elements of Intuitionistic Logic – stackoverflow.com
StackExchange Bot (May 28 2023 at 00:44):shooqie posted a new question on May 28, 2023 at 01:25AM: Set type Variable to a concrete type inside a definition – stackoverflow.com
StackExchange Bot (May 29 2023 at 15:44):Henri_S posted a new question on May 29, 2023 at 05:37PM: Is there a way for Coq to recall it already proved a property for the same element in the same proof? – stackoverflow.com
StackExchange Bot (May 30 2023 at 21:44):epelaez posted a new question on May 30, 2023 at 09:46PM: Implementing variable replacement in a boolean polynomial function in Coq – stackoverflow.com
StackExchange Bot (Jun 01 2023 at 18:44):coqbeginner posted a new question on June 01, 2023 at 08:35PM: Notation problem – cstheory.stackexchange.com
StackExchange Bot (Jun 02 2023 at 15:47):nobody posted a new question on June 02, 2023 at 04:20PM: Including header / footer in a file generated by extraction – stackoverflow.com
StackExchange Bot (Jun 02 2023 at 15:47):Charlie Parker posted a new question on June 02, 2023 at 05:25PM: How to parse coq statements from a coq .v file the official way? – stackoverflow.com
StackExchange Bot (Jun 02 2023 at 17:47):R. Bosman posted a new question on June 02, 2023 at 05:59PM: How to teach crush to unfold definitions? – stackoverflow.com
StackExchange Bot (Jun 04 2023 at 03:44):epelaez posted a new question on June 04, 2023 at 04:48AM: Clear hypotheses after recursive Ltac – stackoverflow.com
StackExchange Bot (Jun 05 2023 at 10:45):Johan Buret posted a new question on June 05, 2023 at 10:46AM: Proving a logic riddle in Coq : testing equivalence in an Inductive set – proofassistants.stackexchange.com
StackExchange Bot (Jun 06 2023 at 00:44):cosmonia posted a new question on June 06, 2023 at 02:10AM: Proving Transitivity of Pointwise Relations on Lists in Coq – stackoverflow.com
StackExchange Bot (Jun 08 2023 at 16:45):lam_gam posted a new question on June 08, 2023 at 05:19PM: How to prove Theorem euclid_gcd : forall a b z, euclid a b z -> gcd a b z. using coq? – stackoverflow.com
StackExchange Bot (Jun 09 2023 at 04:45):Circuit Craft posted a new question on June 09, 2023 at 05:37AM: Induction scheme on two arguments for custom type in Coq – proofassistants.stackexchange.com
StackExchange Bot (Jun 13 2023 at 11:45):Bas Laarakker posted a new question on June 13, 2023 at 12:16PM: Is Prop extensionality inconsistent in Coq? – stackoverflow.com
StackExchange Bot (Jun 13 2023 at 19:45):Farhan posted a new question on June 13, 2023 at 09:37PM: How can I prove Proof Irrelevance from Propositional Extensionality in Coq? – stackoverflow.com
StackExchange Bot (Jun 14 2023 at 09:44):Bruno posted a new question on June 14, 2023 at 11:35AM: Obligation generated by Equations is too strong – proofassistants.stackexchange.com
StackExchange Bot (Jun 14 2023 at 19:45):Moti posted a new question on June 14, 2023 at 08:56PM: Natural deduction in Coq – proofassistants.stackexchange.com
StackExchange Bot (Jun 16 2023 at 01:44):user4614475 posted a new question on June 16, 2023 at 01:56AM: Ergonomic way to define elements of dependent records in proof mode? – stackoverflow.com
StackExchange Bot (Jun 18 2023 at 03:44):dvr posted a new question on June 18, 2023 at 03:57AM: Domain of a map in Coq – stackoverflow.com
StackExchange Bot (Jun 22 2023 at 15:45):Joey Eremondi posted a new question on June 22, 2023 at 05:01PM: Reasoning about CwFs in a proof assistant – proofassistants.stackexchange.com
StackExchange Bot (Jun 23 2023 at 13:45):hmltn posted a new question on June 23, 2023 at 03:35PM: What is the definition of Turing-complete in Coq? – proofassistants.stackexchange.com
StackExchange Bot (Jun 23 2023 at 17:45):7449yyc posted a new question on June 23, 2023 at 05:57PM: Why the Let-in construct cannot be defined as a derived form in a dependently-typed language? – stackoverflow.com
StackExchange Bot (Jun 23 2023 at 21:45):shooqie posted a new question on June 23, 2023 at 11:19PM: Tricks for proving equalities under type cast – proofassistants.stackexchange.com
StackExchange Bot (Jun 24 2023 at 17:45):JoJoModding posted a new question on June 24, 2023 at 07:11PM: Coq's elimination restriction corner cases -- when can you eliminate Prop's into Type? – proofassistants.stackexchange.com
StackExchange Bot (Jun 26 2023 at 20:45):Elad Strasman posted a new question on June 26, 2023 at 09:04PM: coq Constructive mathematics task – stackoverflow.com
StackExchange Bot (Jun 27 2023 at 01:45):7449yyc posted a new question on June 27, 2023 at 03:31AM: What's the role of unification in Coq's core type system? – stackoverflow.com
StackExchange Bot (Jun 27 2023 at 18:44):radrow posted a new question on June 27, 2023 at 07:57PM: Is Prop a subtype of Set? – stackoverflow.com
StackExchange Bot (Jun 29 2023 at 15:45):yiyuan-cao posted a new question on June 29, 2023 at 04:45PM: Programming in Calculus of Inductive Constructions with Coq – stackoverflow.com
StackExchange Bot (Jun 29 2023 at 22:45):Lepticed posted a new question on June 30, 2023 at 12:04AM: Rewrite proposition using equivalence in Coq – stackoverflow.com
StackExchange Bot (Jun 30 2023 at 02:45):yiyuan-cao posted a new question on June 29, 2023 at 04:45PM: Programming in the Calculus of Inductive Constructions with Coq – stackoverflow.com
StackExchange Bot (Jul 08 2023 at 06:44):asha soroushpoor posted a new question on July 08, 2023 at 08:21AM: Defining 2 inductive propositions relying on each other in Coq – cs.stackexchange.com
StackExchange Bot (Jul 09 2023 at 20:44):shooqie posted a new question on July 09, 2023 at 09:17PM: Ltac - run tactic for each hypothesis of given pattern – proofassistants.stackexchange.com
StackExchange Bot (Jul 12 2023 at 07:45):Pietro Braione posted a new question on July 12, 2023 at 09:14AM: How do I debug Gallina (Coq) code? – proofassistants.stackexchange.com
StackExchange Bot (Jul 12 2023 at 10:45):hah posted a new question on July 12, 2023 at 10:44AM: Assistance with Coq: Linking Decidability of Monotonic Enumerations to a Special Principle of Omniscience – stackoverflow.com
StackExchange Bot (Jul 12 2023 at 15:45):matteo_c posted a new question on July 12, 2023 at 05:17PM: Induction error on mutually defined types in Coq – proofassistants.stackexchange.com
StackExchange Bot (Jul 12 2023 at 17:44):asha soroushpoor posted a new question on July 12, 2023 at 05:47PM: Partitioning a list with 2 elements in the middle in coq – proofassistants.stackexchange.com
StackExchange Bot (Jul 14 2023 at 11:45):Pietro Braione posted a new question on July 14, 2023 at 01:01PM: How do I extract efficient string code in Coq to OCaml? – proofassistants.stackexchange.com
StackExchange Bot (Jul 16 2023 at 13:45):Zara posted a new question on July 16, 2023 at 02:01PM: Defining Kripke models and the canonical model for $S4$ modal logic – proofassistants.stackexchange.com
StackExchange Bot (Jul 16 2023 at 15:45):uhbif19 posted a new question on July 16, 2023 at 04:34PM: Formalization of matching logic (logic behind K Framework) – cstheory.stackexchange.com
StackExchange Bot (Jul 16 2023 at 17:45):asha soroushpoor posted a new question on July 16, 2023 at 07:01PM: How to prove commutation of a recursive function over a finite set defined encoded with binary nat – proofassistants.stackexchange.com
StackExchange Bot (Jul 16 2023 at 19:45):asha soroushpoor posted a new question on July 16, 2023 at 07:01PM: How to prove commutation of a recursive function over a finite set encoded with binary nat in coq – proofassistants.stackexchange.com
StackExchange Bot (Jul 16 2023 at 19:45):Pietro Braione posted a new question on July 16, 2023 at 07:48PM: What is the correct way to define a DecidableType module? – proofassistants.stackexchange.com
StackExchange Bot (Jul 17 2023 at 16:45):Pandemonium posted a new question on July 17, 2023 at 05:45PM: Unable to unify "n * 0" with "0" – stackoverflow.com
StackExchange Bot (Jul 20 2023 at 01:44):L-- posted a new question on July 20, 2023 at 02:55AM: PLF: [S <: S->S] Subtyping Example Hint – stackoverflow.com
StackExchange Bot (Jul 20 2023 at 16:44):Lepticed posted a new question on July 20, 2023 at 05:57PM: Coq: A \/ A -> A – stackoverflow.com
StackExchange Bot (Jul 21 2023 at 15:45):toku-sa-n posted a new question on July 21, 2023 at 03:52PM: How to generate the AST of a Coq source code? – stackoverflow.com
StackExchange Bot (Jul 22 2023 at 10:45):asha soroushpoor posted a new question on July 22, 2023 at 12:14PM: How to define induction on arbitrary functions in coq – proofassistants.stackexchange.com
StackExchange Bot (Jul 25 2023 at 09:45):yiyuan-cao posted a new question on July 25, 2023 at 11:02AM: The significance of different types of memory models in low-level language program verification? – cstheory.stackexchange.com
StackExchange Bot (Jul 29 2023 at 06:45):toku-sa-n posted a new question on July 29, 2023 at 07:27AM: How to extract the exact information of GenArg? – stackoverflow.com
StackExchange Bot (Jul 31 2023 at 16:45):noCrayCray posted a new question on July 31, 2023 at 05:59PM: "Expected a single focused goal but 2 goals are focused." error in coq regarding string equality(I think) – proofassistants.stackexchange.com
StackExchange Bot (Jul 31 2023 at 20:46):Julián posted a new question on July 31, 2023 at 10:03PM: Have Hyperdoctrines been formalized? – proofassistants.stackexchange.com
StackExchange Bot (Aug 01 2023 at 03:45):Agnishom Chattopadhyay posted a new question on August 01, 2023 at 04:50AM: Rewriting inside quantified propositions in Coq? – proofassistants.stackexchange.com
StackExchange Bot (Aug 02 2023 at 20:44):Jason Gross posted a new question on August 02, 2023 at 10:08PM: Factoring custom grammar rules for integers and lists in Coq custom entries – proofassistants.stackexchange.com
StackExchange Bot (Aug 03 2023 at 19:44):Lepticed posted a new question on August 03, 2023 at 07:48PM: Forall and exists in a Coq proof – stackoverflow.com
StackExchange Bot (Aug 08 2023 at 15:44):paulotorrens posted a new question on August 08, 2023 at 05:05PM: How to reason about and extract code for inductive types with negative occurrences in Coq? – proofassistants.stackexchange.com
StackExchange Bot (Aug 08 2023 at 15:44):Vladimir Prigodsky posted a new question on August 08, 2023 at 05:14PM: Using CoqHammer from Ltac2 – proofassistants.stackexchange.com
StackExchange Bot (Aug 09 2023 at 01:44):Kyle Lin posted a new question on August 09, 2023 at 02:47AM: Coq: Would adding "inline inductive definition expressions" introduce inconsistency? – proofassistants.stackexchange.com
StackExchange Bot (Aug 11 2023 at 12:45):TomR posted a new question on August 11, 2023 at 01:01PM: Is there formalization of (any) model of ∞-category in (any) proof assistant? And if there is none, what is the challenge of creating one? – proofassistants.stackexchange.com
StackExchange Bot (Aug 12 2023 at 15:46):Julián posted a new question on August 12, 2023 at 05:30PM: How to install dependencies correctly? [Cannot find a physical path bound to logical path] – proofassistants.stackexchange.com
StackExchange Bot (Aug 12 2023 at 19:46):TomR posted a new question on August 12, 2023 at 09:18PM: How to download (e.g. from Github) Coq, if its main site is down? – proofassistants.stackexchange.com
StackExchange Bot (Aug 15 2023 at 09:44):Kyle Lin posted a new question on August 15, 2023 at 09:48AM: Can you always replace mutually recursive references with parameters? – proofassistants.stackexchange.com
StackExchange Bot (Aug 15 2023 at 09:44):Kyle Lin posted a new question on August 15, 2023 at 10:57AM: Why does Coq not allow constructor argument types to be strictly positive mutual inductive types? – proofassistants.stackexchange.com
StackExchange Bot (Aug 15 2023 at 14:45):Gregory Bush posted a new question on August 15, 2023 at 04:12PM: Type-specific proof of UIP for type with decidable equality using induction – stackoverflow.com
StackExchange Bot (Aug 16 2023 at 12:45):vzhilin posted a new question on August 16, 2023 at 02:32PM: List without gaps in Coq – stackoverflow.com
StackExchange Bot (Aug 16 2023 at 20:46):Nicolas Rinaudo posted a new question on August 16, 2023 at 10:29PM: Force Coq to simplify unfalsifiable pattern matches – stackoverflow.com
StackExchange Bot (Aug 17 2023 at 12:44):userl6kgPo0ixv posted a new question on August 17, 2023 at 01:28PM: Proving function existence in Coq – proofassistants.stackexchange.com
StackExchange Bot (Aug 17 2023 at 12:44):noCrayCray posted a new question on August 17, 2023 at 02:31PM: İnduction/inversion and others in coq – proofassistants.stackexchange.com
StackExchange Bot (Aug 17 2023 at 19:46):Agnishom Chattopadhyay posted a new question on August 17, 2023 at 08:30PM: Injectivity, Surjectivity and Smallness on lists of natural numbers imply each other – proofassistants.stackexchange.com
StackExchange Bot (Aug 19 2023 at 10:46):E030E03 posted a new question on August 19, 2023 at 11:54AM: Coq specifying the type of a variable – proofassistants.stackexchange.com
StackExchange Bot (Aug 23 2023 at 12:46):joro posted a new question on August 23, 2023 at 02:31PM: How bad is Coq proving both $T$ and $\lnot T$? – mathoverflow.net
StackExchange Bot (Aug 24 2023 at 18:44):PeterTN posted a new question on August 24, 2023 at 08:20PM: Software Foundations Basics - Theorem lower_grade_lowers need to prove implication Eq = Lt -> Eq = Lt – stackoverflow.com
StackExchange Bot (Aug 26 2023 at 21:46):arshiamoeini posted a new question on August 26, 2023 at 10:52PM: formalization of partial function for counting – cs.stackexchange.com
StackExchange Bot (Aug 27 2023 at 15:47):arshiamoeini posted a new question on August 27, 2023 at 04:47PM: formalization of partial function for counting – proofassistants.stackexchange.com
StackExchange Bot (Aug 27 2023 at 19:45):arshiamoeini posted a new question on August 27, 2023 at 04:47PM: Formalization of partial functions for combinatorial counting – proofassistants.stackexchange.com
StackExchange Bot (Aug 29 2023 at 23:45):acogrunge posted a new question on August 30, 2023 at 01:15AM: false = true problem when solving Lemma in Coq – stackoverflow.com
StackExchange Bot (Aug 31 2023 at 19:44):Agnishom Chattopadhyay posted a new question on August 31, 2023 at 08:56PM: Defining a Recursive Function decreasing on one argument with < and another structurally – proofassistants.stackexchange.com
StackExchange Bot (Sep 01 2023 at 07:45):Andrii Kozytskyi posted a new question on September 01, 2023 at 09:08AM: Specializing forall quantifiers in Coq – proofassistants.stackexchange.com
StackExchange Bot (Sep 05 2023 at 16:44):Circuit Craft posted a new question on September 05, 2023 at 06:21PM: Eliminating dependent destruction in Coq – proofassistants.stackexchange.com
StackExchange Bot (Sep 06 2023 at 16:46):noCrayCray posted a new question on September 06, 2023 at 05:12PM: confused about stlc from Programming Language Foundations – proofassistants.stackexchange.com
StackExchange Bot (Sep 07 2023 at 11:45):Maya posted a new question on September 07, 2023 at 01:32PM: Why does Program Fixpoint leave behind a temporary_proof2_subproof axiom in this example? – proofassistants.stackexchange.com
StackExchange Bot (Sep 10 2023 at 05:44):kunkun posted a new question on September 10, 2023 at 07:03AM: How to proof by natural number case analysis in Coq? – stackoverflow.com
StackExchange Bot (Sep 11 2023 at 23:46):user3598542 posted a new question on September 12, 2023 at 12:40AM: How to represent 2D array in Verifiable C – stackoverflow.com
StackExchange Bot (Sep 12 2023 at 06:45):user1953221 posted a new question on September 12, 2023 at 08:22AM: Understanding TLC's finite map library – stackoverflow.com
StackExchange Bot (Sep 14 2023 at 16:46):jschroed TV posted a new question on September 14, 2023 at 05:57PM: vscoq language server failed installing – stackoverflow.com
StackExchange Bot (Sep 19 2023 at 12:45):Weier posted a new question on September 19, 2023 at 02:27PM: (Dis)Advantages of basing a proof assistant on CH correspondence? – proofassistants.stackexchange.com
StackExchange Bot (Sep 19 2023 at 16:45):someStudentCS posted a new question on September 19, 2023 at 06:36PM: Coq: Cannot infer the type of function in environment – stackoverflow.com
StackExchange Bot (Sep 20 2023 at 08:46):someStudentCS posted a new question on September 19, 2023 at 06:36PM: Cannot infer the type of function in environment – stackoverflow.com
StackExchange Bot (Sep 21 2023 at 17:46):Sam Ni posted a new question on September 21, 2023 at 06:45PM: coq, is there a tartic to auto solve simle inequality such as a < b for real numbers? – stackoverflow.com
StackExchange Bot (Sep 26 2023 at 05:44):Sheldon posted a new question on September 26, 2023 at 06:22AM: iris/algebra/auth.vo has bad version number 81700 (expected 81601) for IRIS Coq – proofassistants.stackexchange.com
Last updated: Sep 26 2023 at 12:02 UTC