Questions tagged [coq-mathcomp]
Mathematical Components are libraries of formalized mathematics developed using the Coq proof assistant.
5
questions
2
votes
0
answers
46
views
SSReflect tuple constructor: why not use phantom?
I was reading the mathcomp book learning about canonical structures and following along with the mathcomp source to compare how things were done in practice. Specifically I was looking at sections 6....
- 21
8
votes
2
answers
650
views
Explanation of Coq math-comp repositories
How are the Coq math-comp account and repositories related?
Details
One of my side goals is to try to keep the tags on this site meaningful and useful.
Today I ran into this question:
How to prove ...
- 2,676
4
votes
1
answer
95
views
How can I prove has_esp when using mathcomp.analysis?
How can I prove the following goal (which I believe to be true) using mathcomp.analysis?
...
- 157
5
votes
2
answers
64
views
How to provide a countType when using mathcomp?
The following snippet can't pass type checking.
From mathcomp Require Import choice.
Definition exfn (A:countType) := false.
(* Fail *) Check exfn nat.
Failed with ...
- 157
7
votes
2
answers
137
views
How to prove `forall m n : nat, m == n -> m = n`?
I am learning Coq with ssreflect. Just to understand things, I've proved forall a b : bool, a == b -> a = b but I can't figure out how to prove ...
- 273