About the Learning category


1

662

February 12, 2019

Using Add Relation for Setoid equivalence of rationals


0

52

April 26, 2022

One weird trick to encode modal types


0

52

April 25, 2022

How to import Basics.v in Induction.v of LF using VS Coq extension


6

112

April 14, 2022

DFA In COQ


5

75

April 13, 2022

Machine learning and hammers for Coq


36

3407

April 7, 2022

Functional induction with remember


2

106

April 1, 2022

Completely confused by a trivial SSR proof with case


3

86

March 30, 2022

Annoying warnings when Requiring/Importing ssreflect


4

68

March 28, 2022

Inductive proof automation


6

525

March 25, 2022

What is a hammer/atp within the logic of coq that does things like induction in coq?


1

69

March 24, 2022

How to state mutual/nested lemmas


8

170

March 22, 2022

Saerch in VSCoq


5

74

March 22, 2022

Stdlib documentation online?


1

65

March 20, 2022

More informative response to stucked proofs?


3

101

March 18, 2022

Indeterminate value for partial functions trick


4

163

March 14, 2022

Stream of nonempty lists to stream


2

94

March 11, 2022

How to have vscode find coq?


3

214

March 10, 2022

Verify a intrusive linked list is memory safe with Coq


4

132

March 7, 2022

How to activate the messages window in vscode like the coqide has?


1

99

March 5, 2022

Help with notations that "look alike"


2

91

March 4, 2022

Coqtop not found


10

1859

March 3, 2022

How to create a Powerset of MSetList?


2

106

February 24, 2022

How to use coqc's `verbose` option?


0

69

February 23, 2022

How to install Coq when it says the repository cannot be found? (e.g. issues with m1 chip mac, apple)


21

353

February 17, 2022

Applying a theorem that doesn't match exactly


4

126

February 6, 2022

How to assume an identifier bound to a type with decidable equality using Coq.Structures.Equalities?


2

144

January 29, 2022

Illformed recursive definition using `let fix`


2

140

January 25, 2022

Building a project with coq_makefile, using a library specified in .coqrc


0

102

January 25, 2022

Prooving the length of a list under constraint


8

230

January 25, 2022
