| changeset 11943 | a9672446b45f |
| parent 11638 | 2c3dee321b4b |
| child 12011 | 1a3a7b3cd9bb |
| 11942:06fac365248d | 11943:a9672446b45f |
|---|---|
13 |
13 |
14 datatype dB = |
14 datatype dB = |
15 Var nat |
15 Var nat |
16 | App dB dB (infixl "$" 200) |
16 | App dB dB (infixl "$" 200) |
17 | Abs dB |
17 | Abs dB |
18 |
|
19 syntax (symbols) |
|
20 App :: "dB => dB => dB" (infixl "\<^sub>\<degree>" 200) |
|
18 |
21 |
19 consts |
22 consts |
20 subst :: "[dB, dB, nat] => dB" ("_[_'/_]" [300, 0, 0] 300) |
23 subst :: "[dB, dB, nat] => dB" ("_[_'/_]" [300, 0, 0] 300) |
21 lift :: "[dB, nat] => dB" |
24 lift :: "[dB, nat] => dB" |
22 |
25 |