|
About the Learning category
|
|
1
|
1072
|
February 12, 2019
|
|
Is there a way to create binary floats from hexadecimals?
|
|
1
|
38
|
April 22, 2024
|
|
Replacing "true = false"
|
|
3
|
93
|
April 11, 2024
|
|
Ologs in Coq
|
|
0
|
68
|
April 10, 2024
|
|
How to simplify single-branch match expressions?
|
|
2
|
74
|
April 8, 2024
|
|
Https://coq.inria.fr/opam/released is down
|
|
3
|
67
|
April 8, 2024
|
|
How to use binary floats in Flocq
|
|
3
|
83
|
April 5, 2024
|
|
How to proof a simple statement about rational numbers
|
|
4
|
120
|
March 26, 2024
|
|
How to automatically extract anonymous subterms in a goal
|
|
0
|
74
|
March 19, 2024
|
|
Ltac with variadic argument
|
|
1
|
140
|
March 4, 2024
|
|
[Question; very basic] Stack-based virtual machine test
|
|
2
|
143
|
March 1, 2024
|
|
Destructing term when match generates equality involving that term
|
|
5
|
133
|
February 20, 2024
|
|
Negative definitions of coinductive propositions
|
|
2
|
128
|
February 19, 2024
|
|
Is constructive indefinite description a conservative extension?
|
|
4
|
125
|
February 13, 2024
|
|
Induction hypotheses, again
|
|
4
|
125
|
February 9, 2024
|
|
Coq examples of cut elimination in sequent calculi?
|
|
2
|
132
|
February 8, 2024
|
|
Simplifying/rewriting inside of an anonymous fixpoint
|
|
0
|
115
|
February 6, 2024
|
|
Dependent-typed terms as return values / function parameters
|
|
3
|
171
|
February 2, 2024
|
|
Coq platform script downloads are triggering my antivirus
|
|
4
|
141
|
January 24, 2024
|
|
Coq/Ocaml project using heuristic function written in C?
|
|
1
|
126
|
January 23, 2024
|
|
Match Case Analysis and Propagation (redux)
|
|
3
|
167
|
January 17, 2024
|
|
Various installation attempts on MacbookPro M3 Max stall or hang
|
|
4
|
182
|
January 15, 2024
|
|
Defining Mutual Induction Principles Manually
|
|
2
|
160
|
January 9, 2024
|
|
How to get rid of warnings like "Warning: Cannot open directory /usr/games/."?
|
|
8
|
186
|
January 5, 2024
|
|
Class/type hierarchies
|
|
7
|
359
|
August 28, 2023
|
|
Do multiple theorems allow the same name?
|
|
1
|
137
|
December 24, 2023
|
|
Trying a Tactic with All Visible Goals
|
|
7
|
148
|
December 22, 2023
|
|
Define inductive branch with constraint on branch parameters
|
|
1
|
105
|
December 22, 2023
|
|
Implicit argument resolution
|
|
3
|
209
|
December 22, 2023
|
|
Software foundations theorem
|
|
1
|
150
|
December 22, 2023
|