gabrielhdt

Set : Type.
injective El : (Set -> Type).


N : Type.
s : N -> N.
z : N.

T : (N -> Type).
cons! : (n : N -> (Set -> ((T n) -> (T (s n))))).

gabrielhdt

constant symbol Set: TYPE;
injective symbol El : Set → TYPE;
notation El prefix 1;

constant symbol o : Set;
injective symbol Prf : El o → TYPE;
notation Prf prefix 1;

constant symbol &-> : Set → Set → Set;
notation &-> infix right 7;

gabrielhdt

// Levels as in agda syntax
constant symbol L : TYPE;
symbol Z : L;
symbol S : L → L;
symbol ∪ : L → L → L; notation ∪ infix right 10;
symbol ⋄ : L → L;


// Nat to count succesors 
constant symbol ℕ : TYPE;

gabrielhdt

#!/bin/gawk -f
## This script flushes left and indents correctly documentation of caml code.
## We modify `RS` and `FS` so awk parses the file function by function
## (separated by newlines) along with their documentation. We then call the
## external program `par` on the comments and print the rest unchanged.
BEGIN {
    # Record separator is gawk empty lines
    RS = "";
    FS = "\n";
    # State variables,

gabrielhdt

package_name = tmp
root_path = tmp