b640fb89ee46f63ae66111c0a12c0ff39e9daf20Christian Maederfree type Bool ::= False | True
5cb757fab60f0c6bd6c2ff444d18963f078be9beChristian Maederop And : Bool -> ? Bool -> Bool
b640fb89ee46f63ae66111c0a12c0ff39e9daf20Christian Maedervar x : ? Bool
b640fb89ee46f63ae66111c0a12c0ff39e9daf20Christian Maeder. And False x = False
b640fb89ee46f63ae66111c0a12c0ff39e9daf20Christian Maeder. And True x = x
b640fb89ee46f63ae66111c0a12c0ff39e9daf20Christian Maeder. And False True = False; %implied
678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maederop And : Bool -> ? Bool -> Bool
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maederop False : Bool %(constructor)%
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maederop True : Bool %(constructor)%
b640fb89ee46f63ae66111c0a12c0ff39e9daf20Christian Maederfree type Bool ::= False | True %(ga_Bool)%
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maederforall x : ? Bool . And False x = False
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maederforall x : ? Bool . And True x = x
021d7137df04ec1834911d99d90243a092841cedChristian Maeder. And False True = False %implied
3aa7e4492a7e28b37d1a0b23f5bfe2109f87d4d6Christian Maeder3.8: ### Hint: not a kind '? Bool'