← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to examples/outdated-and-incorrect/clowns/Clowns.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
examples/outdated-and-incorrect/clowns/Clowns.agda
1
 
{-# OPTIONS --no-positivity-check #-}
2
 
 
3
 
module Clowns where
4
 
 
5
 
import Equality
6
 
import Isomorphism
7
 
import Derivative
8
 
import ChainRule
9
 
open import Sets
10
 
open import Functor
11
 
open import Zipper
12
 
open import Dissect
13
 
 
14
 
open Functor.Recursive
15
 
open Functor.Semantics
16
 
 
17
 
NatF : U
18
 
NatF = K [1] + Id
19
 
 
20
 
Nat : Set
21
 
Nat = μ NatF
22
 
 
23
 
zero : Nat
24
 
zero = inn (inl <>)
25
 
 
26
 
suc : Nat -> Nat
27
 
suc n = inn (inr n)
28
 
 
29
 
plus : Nat -> Nat -> Nat
30
 
plus n m = fold NatF φ n where
31
 
  φ : ⟦ NatF ⟧ Nat -> Nat
32
 
  φ (inl <>) = m
33
 
  φ (inr z)  = suc z
34
 
 
35
 
ListF : (A : Set) -> U
36
 
ListF A = K [1] + K A × Id
37
 
 
38
 
List' : (A : Set) -> Set
39
 
List' A = μ (ListF A)
40
 
 
41
 
nil : {A : Set} -> List' A
42
 
nil = inn (inl <>)
43
 
 
44
 
cons : {A : Set} -> A -> List' A -> List' A
45
 
cons x xs = inn (inr < x , xs >)
46
 
 
47
 
sum : List' Nat -> Nat
48
 
sum = fold (ListF Nat) φ where
49
 
  φ : ⟦ ListF Nat ⟧ Nat -> Nat
50
 
  φ (inl <>) = zero
51
 
  φ (inr < n , m >) = plus n m
52
 
 
53
 
TreeF : U
54
 
TreeF = K [1] + Id × Id
55
 
 
56
 
Tree : Set
57
 
Tree = μ TreeF
58
 
 
59
 
leaf : Tree
60
 
leaf = inn (inl <>)
61
 
 
62
 
node : Tree -> Tree -> Tree
63
 
node l r = inn (inr < l , r >)
64