coq

305 Questions
Newest Active Unanswered Frequent
Score
View
Card Compact
How to solve a simple inequality in COQ with the same variable which is adding on both sides of the inequality
user_170753540
•
1
1
117
coq-tactic coq
How to prove insert_BST in Coq
user_170753540
•
1
2
138
proof-of-correctness coq-tactic coq proof logic
How to solve the very simple Syntax error: 'end' expected after [branches] (in [term_match]). in Coq? (in Gallina and not ltac)
user_16015800
•
2
2
109
coq
Removing the last element of a sized list in Coq
user_124946370
•
1
1
57
coq
Coq proof usage
user_184941280
•
3
1
76
coq-extraction coq
Creating Coq tactic: how to use a newly generated name?
user_50367220
•
3
1
28
coq-tactic coq proof
Why is my local coq no acting the same as standard coq e.g. as JsCoq?
user_16015800
•
2
1
47
jscoq coq-tactic visual-studio-code coq
What does `apply.` tactic on it's own do in Coq -- i.e. without specifying a rule or hypothesis to unify the goal's conclusion with?
user_16015800
•
1
1
57
ssreflect coq-tactic coq
How to tell vscode where Coq is? (fixing Could not start coqtop (coqtop))
user_16015800
•
2
1
370
visual-studio-code coq
Tactic for existential hypothesis
user_5258720
•
1
2
70
coq-tactic coq
Hot Questions