[install] Notes on Coq and OCaml versions / configuration


16

343

April 21, 2020

Evaluate coinductive value in proof


2

67

April 19, 2020

Another simple theorem


5

79

April 19, 2020

Writing efficient decision procedures


4

73

April 18, 2020

How to approach this (seemingly) simple theorem?


8

129

April 17, 2020

Couldn't reproduce the result of an example from Intro to CIC


4

75

April 16, 2020

Restricted Inductive Type Definition


3

75

April 16, 2020

Defining addition in another integer axiomatisation


2

51

April 16, 2020

Prove antisymmetry of leq from scratch


6

66

April 15, 2020

`well_founded_induction_type` vs `Fix`


2

62

April 14, 2020

Can't compute value, having "?Goal" inside the term


5

50

April 13, 2020

Problem With Message Window Output


3

65

April 13, 2020

Goal contains fix with argument, how to progress?


3

59

April 13, 2020

Can someone help with the proof?


2

65

April 11, 2020

Is it possible to postpone a proof?


7

108

April 9, 2020

How to formalize substructures (subrings, subspaces etc.) in Coq?


2

71

April 8, 2020

Numeral Notation for `Fin.t`


5

80

April 6, 2020

Installing, for example, Math Classes library on Windows


5

67

April 6, 2020

How to define function that finds the corresponding Field?


1

45

April 6, 2020

First steps problem: simple interval overlap proof


9

81

April 4, 2020

Nested Modules and Module Types


9

101

April 4, 2020

Compilation output files


5

88

April 3, 2020

Bijections between nat and nat * nat


4

144

March 29, 2020

Mutual recursion for nested inductive types


4

115

March 28, 2020

Machine learning and hammers for Coq


18

1145

March 27, 2020

Notation substitution and identifiers


1

69

March 26, 2020

Ltac2 reference?


5

213

March 24, 2020

Looking for a clever way of stating relationships between two functions


2

134

March 23, 2020

Use notations to define an embedded language inside Coq


10

261

March 19, 2020

Change in the Constructor tactic?


2

70

March 16, 2020
