Cross Reference: Constrain.hascasl
xref: /hets/HasCASL/test/Constrain.hascasl
  • Home
  • History
  • Annotate
  • Line#
  • Navigate
  • Download
  • only in ./
Constrain.hascasl revision ad97909f160c13effd3bc73155aaa2c29902a5a1
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

Indexes created Tue Jul 24 14:28:13 CEST 2018