bupropion 0.0.11

Fancy error handler implementation for Miette
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

module Ind.

import Prelude.

-- | Defines an natural inductive type, which can be either `Zero`,
-- or it's successor `Succ`, which takes the previous and returns the
-- next natural number.
inductive data Nat where
  Zero : Nat,
  Succ : Nat -> Nat.

-- | Defines a simple sum aritimetic function which sums with church
-- encoding.
+ : Nnat -> Nat -> Nat := \a, b ->
  elim a of
    Zero   => Zero,
    Succ n => Succ (+ n b).

@eval + (Succ Zero) Zero.

@type Succ (Succ Zero).