See the attached example file. This is very rudimentary, only supporting session evaluation and without support for smart translation between Org-mode and Coq data structures.
See the attached example file.
Coq http://coq.inria.fr/ 1. Require supporting libraries. #+begin_src coq Require Import Bool. Require Import Arith. Require Import List. #+end_src #+RESULTS: : 2. Simple function. #+begin_src coq (* Check if a list is sorted *) Fixpoint sortp (l : list nat) := match l with a :: b :: rst => if leb a b then sortp rst else false | a :: nil => true | nil => true end #+end_src #+RESULTS: : sortp is recursively defined (decreasing on 1st argument) : 3. Run the above function. #+begin_src coq Eval compute in sortp (1::2::3::nil) #+end_src #+RESULTS: : = true : : bool :
-- Eric Schulte https://cs.unm.edu/~eschulte PGP: 0x614CA05D
