|
How to apply hypothesis with a disjunction?
|
|
3
|
747
|
May 8, 2020
|
|
Why does the entire body of a cofix need to be guarded?
|
|
3
|
767
|
May 6, 2020
|
|
Deprecated
|
|
6
|
904
|
May 6, 2020
|
|
Yet another simple theorem
|
|
8
|
1188
|
May 4, 2020
|
|
Compute a bijection (A <~> B) from a bijection (option A <~> option B)
|
|
6
|
804
|
May 3, 2020
|
|
Asymmetric variant of program equivalence : Program approximation
|
|
4
|
806
|
May 2, 2020
|
|
Extracting strings and ascii
|
|
2
|
1011
|
April 27, 2020
|
|
Implicit arguments in non-top-level functions
|
|
3
|
1137
|
April 24, 2020
|
|
[PG/Company] Structured outline mode
|
|
2
|
513
|
April 23, 2020
|
|
Extensional setoids on functions, and rewriting
|
|
8
|
1805
|
April 22, 2020
|
|
Writing a function to find the head of each item in list of lists
|
|
9
|
1082
|
April 22, 2020
|
|
Best formulation for inductive propositions?
|
|
4
|
596
|
April 21, 2020
|
|
Evaluate coinductive value in proof
|
|
1
|
695
|
April 19, 2020
|
|
Another simple theorem
|
|
4
|
605
|
April 19, 2020
|
|
Writing efficient decision procedures
|
|
3
|
625
|
April 18, 2020
|
|
How to approach this (seemingly) simple theorem?
|
|
7
|
847
|
April 17, 2020
|
|
Couldn't reproduce the result of an example from Intro to CIC
|
|
3
|
870
|
April 16, 2020
|
|
Restricted Inductive Type Definition
|
|
2
|
515
|
April 16, 2020
|
|
Defining addition in another integer axiomatisation
|
|
1
|
495
|
April 16, 2020
|
|
Prove antisymmetry of leq from scratch
|
|
5
|
978
|
April 15, 2020
|
|
`well_founded_induction_type` vs `Fix`
|
|
1
|
733
|
April 14, 2020
|
|
Can't compute value, having "?Goal" inside the term
|
|
4
|
716
|
April 13, 2020
|
|
Problem With Message Window Output
|
|
2
|
540
|
April 13, 2020
|
|
Goal contains fix with argument, how to progress?
|
|
2
|
575
|
April 13, 2020
|
|
Can someone help with the proof?
|
|
1
|
694
|
April 11, 2020
|
|
Is it possible to postpone a proof?
|
|
6
|
1734
|
April 9, 2020
|
|
How to formalize substructures (subrings, subspaces etc.) in Coq?
|
|
1
|
570
|
April 8, 2020
|
|
Numeral Notation for `Fin.t`
|
|
4
|
1126
|
April 6, 2020
|
|
Installing, for example, Math Classes library on Windows
|
|
4
|
777
|
April 6, 2020
|
|
How to define function that finds the corresponding Field?
|
|
0
|
475
|
April 6, 2020
|