From 67b13a5ef9bd35683ed91a39ae004e0fe89ed46a Mon Sep 17 00:00:00 2001
From: Murray Calavera <murray.calavera@protonmail.com>
Date: Wed, 29 Nov 2023 12:31:29 +0000
Subject: [PATCH] coq: init

---
 lang/coq | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100644 lang/coq

diff --git a/lang/coq b/lang/coq
new file mode 100644
index 0000000..e4bd78e
--- /dev/null
+++ b/lang/coq
@@ -0,0 +1,36 @@
+language = "coq"
+name = "Coq"
+homepage = Just "https://coq.inria.fr/"
+spec = Informal
+status = Mainstream
+
+impl = Standalone
+domain = [ ProofAssistant ]
+platform = [ Linux, Windows, MacOS ]
+
+typing = Static
+safety = Verified
+mm = AutomaticMM
+everything = AMess
+
+paradigms = [ Functional ]
+parallelism = [ ]
+features = [ Closures, NominalTyping, TypeInference, ParametricPoly, Dependent ]
+concurrency = [ ]
+runtime = [ Stack, Interpreter, GarbageCollector, ErrorHandling, Unifier ]
+
+orthogonality = Acceptable
+example =
+  """
+  From Coq Require Import ssreflect ssrfun ssrbool.
+  From mathcomp Require Import eqtype ssrnat div prime.
+
+  (* A proof of the infinitude of primes, by Georges Gonthier *)
+  Lemma prime_above m : {p | m < p & prime p}.
+  Proof.
+  have /pdivP[p pr_p p_dv_m1]: 1 < m`! + 1
+    by rewrite addn1 ltnS fact_gt0.
+  exists p => //; rewrite ltnNge; apply: contraL p_dv_m1 => p_le_m.
+  by rewrite dvdn_addr ?dvdn_fact ?prime_gt0 // gtnNdvd ?prime_gt1.
+  Qed.
+  """