|
Strong specification of haskell's Replicate function
|
|
1
|
934
|
May 23, 2021
|
|
Diamond property implies confluence
|
|
11
|
1703
|
May 21, 2021
|
|
Why Coq cannot compute the equality of two Real number (like R1,1,2,3) directly?
|
|
2
|
923
|
May 17, 2021
|
|
Finding the right tactics to proof a theorem
|
|
1
|
533
|
May 10, 2021
|
|
Passing parameters to coqc in dune
|
|
4
|
686
|
April 19, 2021
|
|
Applying a tactic in depth-first manner
|
|
0
|
517
|
April 19, 2021
|
|
Tactics for pattern matching?
|
|
3
|
824
|
April 17, 2021
|
|
Apparently bad installation of coq (im a newbie)
|
|
5
|
1307
|
April 16, 2021
|
|
Proving matrix transpose function
|
|
13
|
1804
|
April 14, 2021
|
|
Turning "exists unique" into a function in Coq
|
|
3
|
1326
|
April 3, 2021
|
|
Bug in the parser?
|
|
5
|
869
|
April 1, 2021
|
|
Not an inductive product
|
|
5
|
1743
|
March 31, 2021
|
|
What axioms are built-in?
|
|
6
|
1797
|
March 31, 2021
|
|
What does `auto` do differently under the hood?
|
|
1
|
779
|
March 31, 2021
|
|
Rtauto slower than tauto
|
|
0
|
511
|
March 29, 2021
|
|
How to express a list of any type X?
|
|
2
|
600
|
March 28, 2021
|
|
Solve an `exists` goal in a field with proof search?
|
|
3
|
1714
|
March 26, 2021
|
|
Reasoning about higher-order program transformation?
|
|
3
|
628
|
March 26, 2021
|
|
Add LoadPath in Coq 8.12.2
|
|
5
|
2409
|
March 22, 2021
|
|
Poll about proofgeneral: do you use "holes"
|
|
0
|
509
|
March 22, 2021
|
|
Defining mathematical function implicitly
|
|
4
|
648
|
March 19, 2021
|
|
Error while installing Coq platform
|
|
2
|
1588
|
March 18, 2021
|
|
avoiding type error
|
|
11
|
741
|
March 11, 2021
|
|
Syntax with backticks
|
|
1
|
601
|
March 11, 2021
|
|
Equality between inductively defined relations
|
|
1
|
586
|
March 7, 2021
|
|
Parametric rewriting under binders
|
|
0
|
754
|
March 3, 2021
|
|
Contradicting instructions for installation with OPAM
|
|
2
|
720
|
March 2, 2021
|
|
Mutual Recursion with function unfolding
|
|
4
|
2703
|
February 13, 2021
|
|
Application of automatic induction principle versus induction tactic
|
|
2
|
695
|
February 7, 2021
|
|
Inversion of an axiom is bad
|
|
6
|
926
|
February 6, 2021
|