| author | paulson |
| Wed, 10 Jan 2001 11:00:17 +0100 | |
| changeset 10840 | 28a53b68a8c0 |
| parent 0 | a5a9c433f639 |
| permissions | -rw-r--r-- |
| 0 | 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 |