About the Learning category


1

549

February 12, 2019

Constructing heterogeneous lists


3

32

October 25, 2021

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


0

14

October 24, 2021

Notation for a coinductive type


0

18

October 22, 2021

Importing with aliasing


2

48

October 16, 2021

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


2

40

October 15, 2021

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


1

59

October 15, 2021

Newbie Needs Tutor on ZOOM


1

56

October 14, 2021

Does Universe Polymorphism extend the theory of Coq?


5

93

October 1, 2021

Overload list notation


3

93

September 27, 2021

Dune + proof general


3

121

September 23, 2021

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


8

95

September 23, 2021

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


1

87

September 22, 2021

Coqtop not found


9

933

September 21, 2021

An awkward inductive definition that resists `destruct`


1

75

September 20, 2021

How to define the SEP(R) clauses?


0

56

September 20, 2021

Awkwardness with coinductive universes


2

84

September 17, 2021

How to use tactic forward_if Q?


4

76

September 16, 2021

How to prove this selfdefined Bag Theorem?


5

183

August 8, 2021

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


2

118

August 5, 2021

Dealing with associativity in reduction relations


4

91

August 1, 2021

Extraction  System error


8

127

July 30, 2021

Software Foundations: minustwo not found in Poly.v


6

116

July 28, 2021

Software Foundations: Normalization Function Exercise


2

88

July 26, 2021

Coq Prove code security


1

118

July 26, 2021

Extraction to Haskell Int type


2

213

July 26, 2021

Evaluating Real numbers to decimal representation


4

182

July 26, 2021

Defining and working with trivial finite sets like {x, y, z} easily


6

145

July 8, 2021

Software foundations: stuck at exercise `binary_inverse` in the Induction chapter


2

120

July 6, 2021

Redefining prod as a record?


1

112

July 4, 2021
