From 91b62765744c8e27320860de9aa08f583b5940f1 Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Tue, 23 Nov 2021 16:31:43 +0100
Subject: [PATCH] removing useless file
---
proofs/src/add-hooks.lisp | 4 ++--
proofs/src/proof-dk.lisp | 9 ---------
2 files changed, 2 insertions(+), 11 deletions(-)
delete mode 100644 proofs/src/proof-dk.lisp
diff --git a/proofs/src/add-hooks.lisp b/proofs/src/add-hooks.lisp
index 7276390..b66fd1b 100644
--- a/proofs/src/add-hooks.lisp
+++ b/proofs/src/add-hooks.lisp
@@ -28,7 +28,7 @@
(with-slots ((goal current-goal) (ctx context) (crule current-rule)) ps
(let* ((forms (mapcar #'formula (s-forms goal)))
(formula (make!-disjunction* forms)))
- (format stream "Prf ~:/pvs:pp-dk/" formula))))
+ (pvs:pp-dk stream formula))))
(defparameter *ps-counter* 0
"Number of proofstates encountered. Used to create identifiers.")
@@ -57,7 +57,7 @@
{ \"name\": name of the proposition,
\"incr\": a unique integer to distinguish the sequents between them,
\"path\": the path from the root to the current proofstate,
- \"dk\": the proposition in Dedukti,
+ \"dk\": the proposition in Dedukti (of type Prop),
\"tac\": some information on the tactic used }"
(let ((elts
`((name . ,(prefix-no-dot (label ps)))
diff --git a/proofs/src/proof-dk.lisp b/proofs/src/proof-dk.lisp
deleted file mode 100644
index 1f9737c..0000000
--- a/proofs/src/proof-dk.lisp
+++ /dev/null
@@ -1,9 +0,0 @@
-;; Use `pp-dk' to print the sequent of proof states as Dedukti propositions.
-(in-package :pvs)
-
-(defun ps->dk (ps)
- "Transform the proofstate PS to a proposition."
- (with-slots ((goal current-goal) (ctx context) (crule current-rule)) ps
- (let* ((forms (mapcar #'formula (s-forms goal)))
- (formula (make!-disjunction* forms)))
- (format nil "Prf ~:/pvs:pp-dk/" formula))))
--
GitLab