HasCASL/test/Constrain.hascasl

	Constrain.hascasl revision ad97909f160c13effd3bc73155aaa2c29902a5a1


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederclass Eq
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederclass Ord < Eq
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedertype a : Ord
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederop f : forall e : Ord . e -> e
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederop c : a
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder. f (f c) = c
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedertype t : Eq
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederop b : t
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder. f b = b