From mboxrd@z Thu Jan  1 00:00:00 1970
From: Eric Schulte <schulte.eric@gmail.com>
Subject: adding rudimentary support for Coq code blocks
Date: Thu, 06 Feb 2014 14:32:12 -0700
Message-ID: <87d2j0c4f3.fsf@gmail.com>
Mime-Version: 1.0
Content-Type: multipart/mixed; boundary="=-=-="
Return-path: <emacs-orgmode-bounces+geo-emacs-orgmode=m.gmane.org@gnu.org>
Received: from eggs.gnu.org ([208.118.235.92]:50493)
	by lists.gnu.org with esmtp (Exim 4.71)
	(envelope-from <schulte.eric@gmail.com>) id 1WBWbk-0001NC-FN
	for emacs-orgmode@gnu.org; Thu, 06 Feb 2014 16:35:44 -0500
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
	(envelope-from <schulte.eric@gmail.com>) id 1WBWbe-00059n-8X
	for emacs-orgmode@gnu.org; Thu, 06 Feb 2014 16:35:40 -0500
Received: from mail-pa0-x232.google.com ([2607:f8b0:400e:c03::232]:33711)
	by eggs.gnu.org with esmtp (Exim 4.71)
	(envelope-from <schulte.eric@gmail.com>) id 1WBWbd-00059N-Vl
	for emacs-orgmode@gnu.org; Thu, 06 Feb 2014 16:35:34 -0500
Received: by mail-pa0-f50.google.com with SMTP id kp14so2243759pab.37
	for <emacs-orgmode@gnu.org>; Thu, 06 Feb 2014 13:35:33 -0800 (PST)
Received: from bagel (c-174-56-50-60.hsd1.nm.comcast.net. [174.56.50.60])
	by mx.google.com with ESMTPSA id sy2sm6698353pbc.28.2014.02.06.13.35.28
	for <emacs-orgmode@gnu.org>
	(version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
	Thu, 06 Feb 2014 13:35:29 -0800 (PST)
List-Id: "General discussions about Org-mode." <emacs-orgmode.gnu.org>
List-Unsubscribe: <https://lists.gnu.org/mailman/options/emacs-orgmode>,
	<mailto:emacs-orgmode-request@gnu.org?subject=unsubscribe>
List-Archive: <http://lists.gnu.org/archive/html/emacs-orgmode>
List-Post: <mailto:emacs-orgmode@gnu.org>
List-Help: <mailto:emacs-orgmode-request@gnu.org?subject=help>
List-Subscribe: <https://lists.gnu.org/mailman/listinfo/emacs-orgmode>,
	<mailto:emacs-orgmode-request@gnu.org?subject=subscribe>
Errors-To: emacs-orgmode-bounces+geo-emacs-orgmode=m.gmane.org@gnu.org
Sender: emacs-orgmode-bounces+geo-emacs-orgmode=m.gmane.org@gnu.org
To: Org Mode Mailing List <emacs-orgmode@gnu.org>

--=-=-=
Content-Type: text/plain

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.


--=-=-=
Content-Type: text/x-org
Content-Disposition: inline; filename=ob-coq-example.org

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
   : 

--=-=-=
Content-Type: text/plain


-- 
Eric Schulte
https://cs.unm.edu/~eschulte
PGP: 0x614CA05D

--=-=-=--