* adding rudimentary support for Coq code blocks
@ 2014-02-06 21:32 Eric Schulte
2014-02-07 15:40 ` Alan Schmitt
0 siblings, 1 reply; 2+ messages in thread
From: Eric Schulte @ 2014-02-06 21:32 UTC (permalink / raw)
To: Org Mode Mailing List
[-- Attachment #1: Type: text/plain, Size: 210 bytes --]
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.
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #2: ob-coq-example.org --]
[-- Type: text/x-org, Size: 680 bytes --]
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
:
[-- Attachment #3: Type: text/plain, Size: 63 bytes --]
--
Eric Schulte
https://cs.unm.edu/~eschulte
PGP: 0x614CA05D
^ permalink raw reply [flat|nested] 2+ messages in thread
* Re: adding rudimentary support for Coq code blocks
2014-02-06 21:32 adding rudimentary support for Coq code blocks Eric Schulte
@ 2014-02-07 15:40 ` Alan Schmitt
0 siblings, 0 replies; 2+ messages in thread
From: Alan Schmitt @ 2014-02-07 15:40 UTC (permalink / raw)
To: Eric Schulte; +Cc: Org Mode Mailing List
Eric Schulte <schulte.eric@gmail.com> writes:
> 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.
Very nice, thanks a lot!
I use org mode with Coq, but only to document Coq developments. See
http://jscert.org/dvpt.html for instance. By the way, I recently
converted two persons to org mode because of its abilities to easily
extract source code to pretty typesetting, both in HTML and LaTeX.
Alan
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~2014-02-07 15:45 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2014-02-06 21:32 adding rudimentary support for Coq code blocks Eric Schulte
2014-02-07 15:40 ` Alan Schmitt
Code repositories for project(s) associated with this public inbox
https://git.savannah.gnu.org/cgit/emacs/org-mode.git
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).