green

uds-psl · Jul 17, 2024 · 94adb57 · 94adb57
1 parent 670003a
commit 94adb57
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git a/coq/arec.v b/coq/arec.v
@@ -1,4 +1,4 @@
-(*** Arithmetic Recursion *)
+(*** MPCTT, Chapter Arithmetic Recursion *)
 From Coq Require Import Lia.
 Definition dec (X: Type) : Type := X + (X -> False).
 Definition eqdec X := forall x y: X, dec (x = y).

diff --git a/coq/solver.v b/coq/solver.v
@@ -1,3 +1,5 @@
+(*** MPCTT, Chapter Propositional Deduction Systems *)
+
 From Coq Require Import List Lia.
 Definition dec (X: Type) : Type := X + (X -> False).
 Definition eqdec X := forall x y: X, dec (x = y).