Skip to content
#

Coq

Star
coq logo

Coq is a formal proof management system. It provides a formal language to write

mathematical definitions, executable algorithms and theorems together with an

environment for semi-interactive development of machine-checked proofs. Typical

applications include the certification of properties of programming languages,

the formalization of mathematics and teaching.

Here are 456 public repositories matching this topic...

Language: All
Filter by language
All 456 Coq 321 OCaml 23 TeX 14 HTML 12 Python 10 Haskell 6 JavaScript 6 Shell 6 Dockerfile 5 Makefile 5
Sort: Best match
Sort options
Best match Most stars Fewest stars Most forks Fewest forks Recently updated Least recently updated

coq / coq

Star
Open

Section variable names and Collection names can clash without warning

11
CohenCyril
CohenCyril commented Nov 2, 2020

Description of the problem

The following code does not raise an error, and the behavior is undocumented.

Section Test.
Variables (b : bool) (n : nat) (All : unit).
Collection n := b.

Lemma foo : True.
Proof using n.
trivial.
Qed.

Lemma bar : True.
Proof using All.
trivial.
Qed.
End Test.

Check foo : bool -> True.
Check bar : bool -> nat -> unit -> True.
Read more
good first issue part: vernac
Find more good first issues →

Created by Gérard Pierre Huet, Thierry Coquand

Released 1989

Latest release 2 days ago

Repository
coq/coq
Website
coq.inria.fr
Wikipedia
Wikipedia
You can’t perform that action at this time.