COQ
1 program
Added 2025-10-22T15:37:16Z
Model: google/gemini-2.5-flashTemp: 0.4
Evidence
Report issue
View issues
Aliases: —
Provenance: commit 5f5c47878f · authored 2025-10-22T17:37:16+02:00 · model google/gemini-2.5-flash
Sources mentioning this language
6 sources · pl_id:
pl/coqWikipedia infobox ↗
Pulled from the
wikimedia/structured-wikipedia
snapshot — see data/raw/wikipedia_pl_facts.*.jsonl and
pl_fact.csv for the long-table provenance.
| Designed by | INRIA · École Polytechnique · University of Paris-Sud · Paris Diderot University · CNRS · ENS Lyon |
|---|---|
| First appeared | 1989 |
| License | LGPLv2.1 |
| Homepage | https://rocq-prover.org |
Extensions claimed by this language
1 claim. Each row is one upstream assertion with its strength.
SWH column shows file occurrences with that extension across the entire archive.| Extension | Source | Strength | SWH |
|---|---|---|---|
.v | pygments | primary | 5.8M files |
Related languages
Rocq (0.10)
LLM-contributed programs
Peano Arithmetic Plus
Provenance: commit 5f5c47878f · authored 2025-10-22T17:37:16+02:00 · model google/gemini-2.5-flash · Temp 0.4
Inductive nat : Set := O : nat | S : nat -> nat.
Definition plus (n m : nat) : nat :=
match n with
| O => m
| S p => S (plus p m)
end.
Lemma plus_O_n : forall n : nat, plus O n = n.
Proof.
intro n.
reflexivity.
Qed.
Lemma plus_S_n : forall n m : nat, plus (S n) m = S (plus n m).
Proof.
intros n m.
reflexivity.
Qed.
Lemma plus_comm : forall n m : nat, plus n m = plus m n.
Proof.
intros n m.
induction n as [| n' IHn'].
- simpl. rewrite plus_O_n. reflexivity.
- simpl. rewrite IHn'. rewrite plus_S_n. reflexivity.
Qed.Real programs from Software Heritage
No SWH evidence indexed yet for this language. (Either the SWH mining hasn't reached this language's extensions, or no matching files exist in the archive.)