1 | theory Second_Steps imports Main |
---|
2 | begin |
---|
3 | ML{* |
---|
4 | val pretty_term = Syntax.pretty_term |
---|
5 | val pwriteln = Pretty.writeln |
---|
6 | fun pretty_terms ctxt ts = |
---|
7 | Pretty.block |
---|
8 | (Pretty.commas (map (pretty_term ctxt) ts)) |
---|
9 | *} |
---|
10 | (* Chapter 3 *) |
---|
11 | (* Section 1: Terms and Types *) |
---|
12 | ML{*@{term "(a::nat) + b = c"}*} |
---|
13 | ML{*@{term "\<lambda>x y. x y"}*} |
---|
14 | ML{*let |
---|
15 | val v1 = Var (("x", 3), @{typ bool}) |
---|
16 | val v2 = Var (("x1", 3), @{typ bool}) |
---|
17 | val v3 = Free ("x", @{typ bool}) |
---|
18 | in |
---|
19 | pretty_terms @{context} [v1, v2, v3] |
---|
20 | |> pwriteln |
---|
21 | end*} |
---|
22 | end |
---|