[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[O] adding rudimentary support for Coq code blocks
From: |
Eric Schulte |
Subject: |
[O] adding rudimentary support for Coq code blocks |
Date: |
Thu, 06 Feb 2014 14:32:12 -0700 |
User-agent: |
Gnus/5.13 (Gnus v5.13) Emacs/24.3 (gnu/linux) |
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
- [O] adding rudimentary support for Coq code blocks,
Eric Schulte <=