About the Learning category


1

561

February 12, 2019

Failing to prove that substituting "by hand" is equivalent to... well, substituting


2

59

November 13, 2021

Existentially quantified coinductive predicates


2

76

November 5, 2021

Notation for a coinductive type


1

62

November 4, 2021

'rewrite' doesn't want to match large expression


1

43

November 2, 2021

Tvals in my code is the total map, why coq insists it is not?


3

60

November 2, 2021

Constructing heterogeneous lists


4

73

October 26, 2021

Thinking of using hammer/automation to guide the order of proving lemmas


0

55

October 24, 2021

Importing with aliasing


2

61

October 16, 2021

Definitions completed with proof scripts are opaque, how to make them compute


2

63

October 15, 2021

Instances created with ':= ltac:(_)' are much slower than Definitions


1

75

October 15, 2021

Newbie Needs Tutor on ZOOM


1

81

October 14, 2021

Does Universe Polymorphism extend the theory of Coq?


5

114

October 1, 2021

Overload list notation


3

106

September 27, 2021

Dune + proof general


3

141

September 23, 2021

Why the tactic "apply... with..." cannot be applied to hypotheses?


8

111

September 23, 2021

Can the Equations plugin generate a graph that does not reference the original function?


1

97

September 22, 2021

Coqtop not found


9

1100

September 21, 2021

An awkward inductive definition that resists `destruct`


1

87

September 20, 2021

How to define the SEP(R) clauses?


0

65

September 20, 2021

Awkwardness with coinductive universes


2

94

September 17, 2021

How to use tactic forward_if Q?


4

105

September 16, 2021

How to prove this selfdefined Bag Theorem?


5

237

August 8, 2021

A question of understanding the paper "Parametric HigherOrder Abstract Syntax for Mechanized Semantics"


2

131

August 5, 2021

Dealing with associativity in reduction relations


4

98

August 1, 2021

Extraction  System error


8

141

July 30, 2021

Software Foundations: minustwo not found in Poly.v


6

133

July 28, 2021

Software Foundations: Normalization Function Exercise


2

103

July 26, 2021

Coq Prove code security


1

135

July 26, 2021

Extraction to Haskell Int type


2

220

July 26, 2021
