-
Notifications
You must be signed in to change notification settings - Fork 2
/
all_libs.typ
101 lines (91 loc) · 3.09 KB
/
all_libs.typ
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
(** Tutorial *)
include "tutorial.typ"
(** Standard library *)
(* simple, common types and function (booleans, option, ...) *)
include "prelude.typ"
(* unary natural numbers *)
include "nat.typ"
(* usual list type *)
include "list.typ"
(* supertype of lists with constant time concatenation *)
include "applist.typ"
(* naive implementation lists *)
include "assoc.typ"
(* set with unbalanced binary search tree *)
include "set.typ"
(* binary representation of natural numbers *)
include "natbin.typ"
(* streams (or infinite lists) *)
include "stream.typ"
(* alternative representation of streams, using an internal state *)
include "state_stream.typ"
(* state monad with an association list as state *)
include "state_array.typ"
(* maps implemented using 2-3 trees *)
include "tree23.typ"
(* trie data structure with basic operations *)
include "trie.typ"
(* unary representation of integers (supertype of nat, no trailing zero) *)
include "int.typ"
(* signed digit representation of real numbers (following Alex Simpson) *)
include "real.typ"
(** Sorting functions on lists *)
(* size-preserving insertion sort *)
include "insert_sort.typ"
(* quicksort function *)
include "quick_sort.typ"
(* heapsort function *)
include "heap_sort.typ"
(** Church encoding examples *)
(* Church-encoded booleans *)
include "church/bool.typ"
(* Church naturals *)
include "church/nat.typ"
(* Church-encoded sums and products *)
include "church/data.typ"
(* Church-encoded lists *)
include "church/list.typ"
(* Church-encoded error monad (option type) *)
include "church/error.typ"
(* Church-encoded state monad *)
include "church/state.typ"
(* Church-encoded streams (infinite lists) *)
include "church/stream.typ"
(* infimum on Church numeral by René David *)
include "church/david.typ"
(** Scott encoding examples *)
(* Scott-encoded natural numbers *)
include "scott/nat.typ"
(* Scott-encoded lists *)
include "scott/list.typ"
(* Scott-encoded streams (inifinte lists) *)
include "scott/stream.typ"
(* binary representation of natural numbers *)
include "scott/natbin.typ"
(* Scott-like encoded for binary trees *)
include "scott/tree.typ"
(* other encoding Scott naturals using records *)
include "scott/nat_as_prod.typ"
(** Other examples of interest *)
(* terminating function not satisfying the usual semi-continuity condition *)
include "hard.typ"
(* lazy variant of unary natural numbers (interesting for termination) *)
include "lazy_nat.typ"
(* filters on streams (using mixed inductive and coinductive types) *)
include "stream_filter.typ"
(* type of ordinals with specific addition functions *)
include "ordinal.typ"
(* λ-calculus using parametric higher-order abstract syntax *)
include "lambda.typ"
(* simply-typed λ-calculus *)
include "simply.typ"
(* red-black trees as a subtype of binary trees *)
include "tree.typ"
(* illustration of the dot-projection for abstract types *)
include "dotproj.typ"
(* other formulation of the dot projection using epsilons *)
include "dotprojeps.typ"
(* addition function with permuted arguments (interesting for termination) *)
include "permute.typ"
(* various examples with sized-types *)
include "size.typ"