What is unsafe about the Ltac2.Constr.Unsafe module?
|
|
2
|
431
|
September 23, 2022
|
Modules vs. generalized rewrite
|
|
4
|
440
|
September 19, 2022
|
Best way to express that a type is inhabited in a way that allows getting the habitant
|
|
1
|
377
|
September 13, 2022
|
Divmod equation
|
|
3
|
433
|
September 11, 2022
|
Defining functions in proof mode
|
|
6
|
699
|
September 9, 2022
|
"Qed." takes a long time
|
|
7
|
745
|
September 1, 2022
|
Coq and denotational semantics
|
|
1
|
364
|
August 27, 2022
|
Efficient algorithms using tree
|
|
6
|
452
|
August 21, 2022
|
Choosing between SProp and axiomatic proof irrelevance
|
|
11
|
755
|
August 16, 2022
|
Is there a solution for the problematic induction hypotheses generated using eqn:H?
|
|
10
|
671
|
August 15, 2022
|
Print Module [Type] lacks types
|
|
0
|
339
|
August 14, 2022
|
Speed of Program Instance
|
|
0
|
301
|
August 12, 2022
|
"Correct" way to structure modules
|
|
2
|
461
|
August 9, 2022
|
The reference omega was not found in the current environment
|
|
2
|
806
|
August 1, 2022
|
Is it possible to suppose the falsity of the goal and prove False in Coq?
|
|
5
|
874
|
July 28, 2022
|
Reusing values from inductive relation
|
|
2
|
380
|
July 24, 2022
|
How to unset printing everything? (e.g. implicits, notations, etc)
|
|
5
|
932
|
June 25, 2021
|
Parsing Tactics via SerAPI
|
|
5
|
708
|
July 15, 2022
|
Indiscernibility of bisimilar coinductive values: can I prove it?
|
|
9
|
321
|
July 12, 2022
|
Using Coq platform on Mac
|
|
1
|
460
|
July 7, 2022
|
SProp question: What can I actually do with a (Squash P) value?
|
|
2
|
440
|
July 7, 2022
|
Setoid_rewrite failed, but succeeded when using '<-' or 'at'
|
|
3
|
459
|
June 25, 2022
|
Apply: versus apply
|
|
4
|
568
|
June 24, 2022
|
[install] Notes on OCaml versions and Coq configuration
|
|
21
|
2858
|
June 21, 2022
|
Decidable equality with Prop-carrying type
|
|
2
|
588
|
June 12, 2022
|
Machine learning and hammers for Coq
|
|
45
|
6529
|
June 6, 2022
|
Induction hypothesis vs. termination checker
|
|
2
|
380
|
June 5, 2022
|
Using Add Relation for Setoid equivalence of rationals
|
|
0
|
447
|
April 26, 2022
|
One weird trick to encode modal types
|
|
0
|
434
|
April 25, 2022
|
DFA In COQ
|
|
5
|
557
|
April 13, 2022
|