diff options
Diffstat (limited to 'generic/pg-pamacs.el')
| -rw-r--r-- | generic/pg-pamacs.el | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el index c8bac3a5..de05c04d 100644 --- a/generic/pg-pamacs.el +++ b/generic/pg-pamacs.el @@ -65,6 +65,12 @@ This macro should only be invoked once a specific prover is engaged." `(symbol-value (intern (concat (symbol-name proof-assistant-symbol) "-" (symbol-name ',sym))))) +(defun proof-ass-differs-from-default (sym) + "Return non-nil if SYM for current prover differs from its customize standard value." + (let ((pasym (proof-ass-symv sym))) + (not (equal (eval (car (get pasym 'standard-value))) + (symbol-value pasym))))) + (defun proof-defpgcustom-fn (sym args) "Define a new customization variable <PA>-sym for current proof assistant. Helper for macro `defpgcustom'." |