Plaster

#| addition.v: Inductive nat : Set := | Z : nat | Suc : nat -> nat. Fixpoint add (a b : nat) : nat := match a with | Z => b | Suc a' => Suc (add a' b) end. Lemma zero_is_identity : forall a : nat, a = (add a Z). intro a. elim a. simpl; auto. simpl; auto. intros. f_equal. assumption. Qed. Require Extraction. Extraction Language JSON. Extraction "/tmp/addition.json" add nat. |# CL-USER> (coq:coq "/tmp/addition.json" (add "add" a b)) WARNING: redefining COMMON-LISP-USER::COPY-Z in DEFUN WARNING: redefining COMMON-LISP-USER::Z-P in DEFUN WARNING: redefining COMMON-LISP-USER::Z in DEFUN WARNING: redefining COMMON-LISP-USER::COPY-SUC in DEFUN WARNING: redefining COMMON-LISP-USER::SUC-P in DEFUN WARNING: redefining COMMON-LISP-USER::SUC-$0 in DEFUN WARNING: redefining COMMON-LISP-USER::SUC in DEFUN WARNING: redefining COMMON-LISP-USER::ADD in DEFUN ("add" "Suc" "Z") CL-USER> (add (suc (suc (suc (z)))) (suc (z))) #S(SUC :$0 #S(SUC :$0 #S(SUC :$0 #S(SUC :$0 #S(Z)))))