<commit_before><!DOCTYPE html>
<html>
 <head>
  <meta charset="utf-8">
  <title>Emanuel: the Epigram manual</title>
 </head>
 <body>
  <header>
    <h1>Emanuel</h1>
    <h2><i>the Epigram manual</i></h2>
  </header>
  <section>
   <h3>Chapter 1 - Introduction</h3>
   <p> Epigram 2 is intended to be a full-scale dependently typed
    programming language in the spirit of Epigram 1 and Agda. It isn't
    finished yet. This document explains how to interact with the
    system as it exists at the moment.
   </p>
   <p>
    Work on the high level programming language has just started. In
    the meantime we can write programs in a more low level fashion
    using Cochon. Cochon looks more like a theorem prover than
    a programming IDE and it's quite low level: the guts are
    showing. Read on for a tutorial of how to write some simple
    programs in Cochon. For a glossary of Cochon commands skip to the
    appendix.
   </p>
  </section>
  <section>
   <h3>Chapter 2 - Installation</h3>
   <p>
    For downloading and installing Epigram see 
    <a href="../web/download.html">look here</a>.
   </p>
  </section>
  <section>
   <h3>Chapter 3 - Running Epigram</h3>
   <p>
    For the moment we interact with Epigram using the Cochon
    interactive theorem prover:
   </p>
   <p>
    <code>$ cd Pig09/src</code><br>
    <code>$ ./Pig</code>
   </p>
   <p>Cochon responds with a prompt:</p>
   <p><code>&gt; _</code></p>
   <p>To exit Cochon you can type
   <p><code>&gt; quit_</code>
   <p>and press return.</p>
  </section>
  <section>
   <h3>Chapter 4 - My first Epigram Program: 2 + 2</h3>
   <p>
    As a first warm-up exercise we will perform the arithmetic feat of
    adding two and two. First of all let's define the natural numbers
    in Peano style. Enter the following at Cochon's prompt and press
    return:
   </p>
   <p><code>&gt; data Nat := ('zero : Nat) ; ('suc : Nat -&gt; Nat)</code></p>
   <p>We defined a new data type <code>Nat</code> and with two
   constructors <code>'zero</code> which takes no arguments
   and <code>'suc</code> which takes a natural number and gives us
   back another natural number. The <code>'</code> is Epigram's
   current notation for a constructor name. There are two canonical
   forms of natural number: either it's zero; or it's the successor of
   another natural number. When we define a datatype in Epigram, and
   give constructors for its canonical forms, we are automatically
   given a computation mechanism (an elimination principle) which says
   that if we want to write a program that consumes elements of that
   datatype we need only explain what to do for its canonical
   forms. This is because any element of a datatype is equal to an
   element in canonical form.
   </p><commit_msg>added pigmode to the running epigram section of the manual<commit_after><!DOCTYPE html>
<html>
 <head>
  <meta charset="utf-8">
  <title>Emanuel: the Epigram manual</title>
 </head>
 <body>
  <header>
    <h1>Emanuel</h1>
    <h2><i>the Epigram manual</i></h2>
  </header>
  <section>
   <h3>Chapter 1 - Introduction</h3>
   <p> Epigram 2 is intended to be a full-scale dependently typed
    programming language in the spirit of Epigram 1 and Agda. It isn't
    finished yet. This document explains how to interact with the
    system as it exists at the moment.
   </p>
   <p>
    Work on the high level programming language has just started. In
    the meantime we can write programs in a more low level fashion
    using Cochon. Cochon looks more like a theorem prover than
    a programming IDE and it's quite low level: the guts are
    showing. Read on for a tutorial of how to write some simple
    programs in Cochon. For a glossary of Cochon commands skip to the
    appendix.
   </p>
  </section>
  <section>
   <h3>Chapter 2 - Installation</h3>
   <p>
    For downloading and installing Epigram see 
    <a href="../web/download.html">look here</a>.
   </p>
  </section>
  <section>
   <h3>Chapter 3 - Running Epigram</h3>
   <p>
    For the moment we interact with Epigram using the Cochon
    interactive theorem prover. You can invoke it directly at the command line:
   </p>
   <p>
    <code>$ Pig</code>
   </p>
   <p>Cochon responds with a prompt:</p>
   <p><code>&gt; _</code></p>
   <p>To exit Cochon you can type
   <p><code>&gt; quit_</code>
   <p>and press return.</p>

   <p>You can also run it in emacs if you insert something like this
   in your <code>.emacs</code>:</p>
   <p><code>(load "/home/dave/Pig09/pigmode.el")</code></p>
   <p>This gives some syntax highlighting for <code>.pig</code>
   files. With the cursor on the first line of a pig file, press C-c
   C-r. This will open a seperate emacs 'window' containing Cochon and
   send the first line of your file to it. Further presses of C-c C-r
   will send subsequent lines. We can interact with (and quit!)
   Cochon in its emacs window just as we did from the command
   line.</p> Have a look in the <code>test</code> directory for some
   sample pig files.
  </section>
  <section>
   <h3>Chapter 4 - My first Epigram Program: 2 + 2</h3>
   <p>
    As a first warm-up exercise we will perform the arithmetic feat of
    adding two and two. First of all let's define the natural numbers
    in Peano style. Enter the following at Cochon's prompt and press
    return:
   </p>
   <p><code>&gt; data Nat := ('zero : Nat) ; ('suc : Nat -&gt; Nat)</code></p>
   <p>We defined a new data type <code>Nat</code> and with two
   constructors <code>'zero</code> which takes no arguments
   and <code>'suc</code> which takes a natural number and gives us
   back another natural number. The <code>'</code> is Epigram's
   current notation for a constructor name. There are two canonical
   forms of natural number: either it's zero; or it's the successor of
   another natural number. When we define a datatype in Epigram, and
   give constructors for its canonical forms, we are automatically
   given a computation mechanism (an elimination principle) which says
   that if we want to write a program that consumes elements of that
   datatype we need only explain what to do for its canonical
   forms. This is because any element of a datatype is equal to an
   element in canonical form.
   </p>
{'fraction_non_alphanumeric': 0.09585533685389662, 'fraction_numerical': 0.007361177788446151, 'mean_word_length': 3.111842105263158, 'pattern_counts': {'":': 0, '<': 166, '<?xml version=': 0, '>': 166, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1141624', 'n_tokens_mistral': 2000, 'n_tokens_neox': 1920, 'n_words': 873}