| changeset 0 | a5a9c433f639 |
| -1:000000000000 | 0:a5a9c433f639 |
|---|---|
1 (* Title: CTT/bool |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1991 University of Cambridge |
|
5 |
|
6 The two-element type (booleans and conditionals) |
|
7 *) |
|
8 |
|
9 Bool = CTT + |
|
10 |
|
11 consts Bool :: "t" |
|
12 true,false :: "i" |
|
13 cond :: "[i,i,i]=>i" |
|
14 rules |
|
15 Bool_def "Bool == T+T" |
|
16 true_def "true == inl(tt)" |
|
17 false_def "false == inr(tt)" |
|
18 cond_def "cond(a,b,c) == when(a, %u.b, %u.c)" |
|
19 end |