Prelude/Bool.ad

Outline
module Prelude.Bool
Bool (datatype)
not (declaration)
Default Bool (typeclass-instance)
boolCase (declaration + definition)
not (definition)
&& (declaration + definition)
|| (declaration + definition)
--> (declaration + definition)
<-> (declaration + definition)
<-/-> (declaration + definition)
Prop (type)
true (declaration)
false (declaration)
bool2prop (declaration + definition)
notP (declaration)
/\ (declaration)
\/ (declaration)
==> (declaration)
<=> (declaration)
<=/=> (declaration)
forallP_fun (declaration)
existsP_fun (declaration)
uexistsP_fun (declaration)

Content
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74

module Prelude.Bool (
  type Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable(..)case-constant `caseBool`
constructor `False`
constructor `True`
,
  boolCaseconstant `Prelude.Bool.boolCase`
   constant
   type `Bool -> 'a -> 'a -> 'a`
   executable,
  notconstant `Prelude.Bool.not`
   constant
   type `Bool -> Bool`
   executable, (&&)constant `Prelude.Bool.(&&)`
   constant
   type `Bool -> Bool -> Bool`
   executable, (||)constant `Prelude.Bool.(||)`
   constant
   type `Bool -> Bool -> Bool`
   executable,
  (-->)constant `Prelude.Bool.(-->)`
   constant
   type `Bool -> Bool -> Bool`
   executable, (<->)constant `Prelude.Bool.(<->)`
   constant
   type `Bool -> Bool -> Bool`
   executable, (<-/->)constant `Prelude.Bool.(<-/->)`
   constant
   type `Bool -> Bool -> Bool`
   executable,

  type Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable,
  trueconstant `Prelude.Bool.true`
   constant
   type `Prop`
   non-executable, falseconstant `Prelude.Bool.false`
   constant
   type `Prop`
   non-executable,
  notPconstant `Prelude.Bool.notP`
   constant
   type `Prop -> Prop`
   non-executable, (/\)constant `Prelude.Bool.(/\)`
   constant
   type `Prop -> Prop -> Prop`
   non-executable, (\/)constant `Prelude.Bool.(\/)`
   constant
   type `Prop -> Prop -> Prop`
   non-executable, (==>)constant `Prelude.Bool.(==>)`
   constant
   type `Prop -> Prop -> Prop`
   non-executable, (<=>)constant `Prelude.Bool.(<=>)`
   constant
   type `Prop -> Prop -> Prop`
   non-executable, (<=/=>)constant `Prelude.Bool.(<=/=>)`
   constant
   type `Prop -> Prop -> Prop`
   non-executable,
  bool2propconstant `Prelude.Bool.bool2prop`
   constant
   type `Bool -> Prop`
   non-executable,

  forallP_funconstant `Prelude.Bool.forallP_fun`
   constant
   type `('a -> Prop) -> Prop`
   non-executable,
  existsP_funconstant `Prelude.Bool.existsP_fun`
   constant
   type `('a -> Prop) -> Prop`
   non-executable,
  uexistsP_funconstant `Prelude.Bool.uexistsP_fun`
   constant
   type `('a -> Prop) -> Prop`
   non-executable
) where

{-# NoImplicitPrelude #-}

import Prelude.Default
{-# allow-similar-names "False", "True", "true", "false" #-}

datatype Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable := False | True
declare notconstant `Prelude.Bool.not`
   constant
   type `Bool -> Bool`
   executable :: Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable -> Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable

instance Defaulttype-class `Prelude.Default.Default`
   arguments: ('a :: *)
   has default derive templates Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable where
end-instance

declare boolCaseconstant `Prelude.Bool.boolCase`
   constant
   type `Bool -> 'a -> 'a -> 'a`
   executable :: Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable -> 'atype-variable `'a`
   kind `*` -> 'atype-variable `'a`
   kind `*` -> 'atype-variable `'a`
   kind `*`
define boolCaseconstant `Prelude.Bool.boolCase`
   constant
   type `Bool -> 'a -> 'a -> 'a`
   executable Trueconstant `Prelude.Bool.True`
   constructor of datatype `Bool`
   type `Bool`
   executable ctvariable `ct`
   type `'a` _ := ctvariable `ct`
   type `'a`
     | boolCaseconstant `Prelude.Bool.boolCase`
   constant
   type `Bool -> 'a -> 'a -> 'a`
   executable Falseconstant `Prelude.Bool.False`
   constructor of datatype `Bool`
   type `Bool`
   executable _ cfvariable `cf`
   type `'a` := cfvariable `cf`
   type `'a`

define notconstant `Prelude.Bool.not`
   constant
   type `Bool -> Bool`
   executable Trueconstant `Prelude.Bool.True`
   constructor of datatype `Bool`
   type `Bool`
   executable := Falseconstant `Prelude.Bool.False`
   constructor of datatype `Bool`
   type `Bool`
   executable
     | notconstant `Prelude.Bool.not`
   constant
   type `Bool -> Bool`
   executable Falseconstant `Prelude.Bool.False`
   constructor of datatype `Bool`
   type `Bool`
   executable := Trueconstant `Prelude.Bool.True`
   constructor of datatype `Bool`
   type `Bool`
   executable

declare (&&)constant `Prelude.Bool.(&&)`
   constant
   type `Bool -> Bool -> Bool`
   executable :: Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable -> Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable -> Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable
define (&&)constant `Prelude.Bool.(&&)`
   constant
   type `Bool -> Bool -> Bool`
   executable Trueconstant `Prelude.Bool.True`
   constructor of datatype `Bool`
   type `Bool`
   executable bvariable `b`
   type `Bool` := bvariable `b`
   type `Bool`
     | (&&)constant `Prelude.Bool.(&&)`
   constant
   type `Bool -> Bool -> Bool`
   executable Falseconstant `Prelude.Bool.False`
   constructor of datatype `Bool`
   type `Bool`
   executable _ := Falseconstant `Prelude.Bool.False`
   constructor of datatype `Bool`
   type `Bool`
   executable

declare (||)constant `Prelude.Bool.(||)`
   constant
   type `Bool -> Bool -> Bool`
   executable :: Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable -> Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable -> Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable
define (||)constant `Prelude.Bool.(||)`
   constant
   type `Bool -> Bool -> Bool`
   executable Trueconstant `Prelude.Bool.True`
   constructor of datatype `Bool`
   type `Bool`
   executable _ := Trueconstant `Prelude.Bool.True`
   constructor of datatype `Bool`
   type `Bool`
   executable
     | (||)constant `Prelude.Bool.(||)`
   constant
   type `Bool -> Bool -> Bool`
   executable Falseconstant `Prelude.Bool.False`
   constructor of datatype `Bool`
   type `Bool`
   executable bvariable `b`
   type `Bool` := bvariable `b`
   type `Bool`

declare (-->)constant `Prelude.Bool.(-->)`
   constant
   type `Bool -> Bool -> Bool`
   executable :: Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable -> Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable -> Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable
define (-->)constant `Prelude.Bool.(-->)`
   constant
   type `Bool -> Bool -> Bool`
   executable b1variable `b1`
   type `Bool` b2variable `b2`
   type `Bool`  := notconstant `Prelude.Bool.not`
   constant
   type `Bool -> Bool`
   executable b1variable `b1`
   type `Bool` ||constant `Prelude.Bool.(||)`
   constant
   type `Bool -> Bool -> Bool`
   executable b2variable `b2`
   type `Bool`

declare (<->)constant `Prelude.Bool.(<->)`
   constant
   type `Bool -> Bool -> Bool`
   executable :: Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable -> Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable -> Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable
define (<->)constant `Prelude.Bool.(<->)`
   constant
   type `Bool -> Bool -> Bool`
   executable b1variable `b1`
   type `Bool` b2variable `b2`
   type `Bool` :=
  (b1variable `b1`
   type `Bool` -->constant `Prelude.Bool.(-->)`
   constant
   type `Bool -> Bool -> Bool`
   executable b2variable `b2`
   type `Bool`) &&constant `Prelude.Bool.(&&)`
   constant
   type `Bool -> Bool -> Bool`
   executable (b2variable `b2`
   type `Bool` -->constant `Prelude.Bool.(-->)`
   constant
   type `Bool -> Bool -> Bool`
   executable b1variable `b1`
   type `Bool`)

declare (<-/->)constant `Prelude.Bool.(<-/->)`
   constant
   type `Bool -> Bool -> Bool`
   executable :: Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable -> Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable -> Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable
define (<-/->)constant `Prelude.Bool.(<-/->)`
   constant
   type `Bool -> Bool -> Bool`
   executable b1variable `b1`
   type `Bool` b2variable `b2`
   type `Bool` := notconstant `Prelude.Bool.not`
   constant
   type `Bool -> Bool`
   executable (b1variable `b1`
   type `Bool` <->constant `Prelude.Bool.(<->)`
   constant
   type `Bool -> Bool -> Bool`
   executable b2variable `b2`
   type `Bool`)

type non-exec Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable

declare non-exec trueconstant `Prelude.Bool.true`
   constant
   type `Prop`
   non-executable  :: Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable
declare non-exec falseconstant `Prelude.Bool.false`
   constant
   type `Prop`
   non-executable :: Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable

declare non-exec bool2propconstant `Prelude.Bool.bool2prop`
   constant
   type `Bool -> Prop`
   non-executable :: Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable -> Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable
define non-exec bool2propconstant `Prelude.Bool.bool2prop`
   constant
   type `Bool -> Prop`
   non-executable bvariable `b`
   type `Bool` := if bvariable `b`
   type `Bool` then trueconstant `Prelude.Bool.true`
   constant
   type `Prop`
   non-executable else falseconstant `Prelude.Bool.false`
   constant
   type `Prop`
   non-executable


declare non-exec notPconstant `Prelude.Bool.notP`
   constant
   type `Prop -> Prop`
   non-executable   :: Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable -> Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable
declare non-exec (/\)constant `Prelude.Bool.(/\)`
   constant
   type `Prop -> Prop -> Prop`
   non-executable   :: Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable -> Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable -> Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable
declare non-exec (\/)constant `Prelude.Bool.(\/)`
   constant
   type `Prop -> Prop -> Prop`
   non-executable   :: Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable -> Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable -> Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable
declare non-exec (==>)constant `Prelude.Bool.(==>)`
   constant
   type `Prop -> Prop -> Prop`
   non-executable  :: Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable -> Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable -> Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable
declare non-exec (<=>)constant `Prelude.Bool.(<=>)`
   constant
   type `Prop -> Prop -> Prop`
   non-executable  :: Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable -> Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable -> Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable
declare non-exec (<=/=>)constant `Prelude.Bool.(<=/=>)`
   constant
   type `Prop -> Prop -> Prop`
   non-executable  :: Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable -> Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable -> Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable

{-# allow-similar-names "forallP_fun", "existsP_fun", "uexistsP_fun" #-}
declare non-exec forallP_funconstant `Prelude.Bool.forallP_fun`
   constant
   type `('a -> Prop) -> Prop`
   non-executable :: ('atype-variable `'a`
   kind `*` -> Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable) -> Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable
declare non-exec existsP_funconstant `Prelude.Bool.existsP_fun`
   constant
   type `('a -> Prop) -> Prop`
   non-executable :: ('atype-variable `'a`
   kind `*` -> Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable) -> Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable
declare non-exec uexistsP_funconstant `Prelude.Bool.uexistsP_fun`
   constant
   type `('a -> Prop) -> Prop`
   non-executable :: ('atype-variable `'a`
   kind `*` -> Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable) -> Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable

end-moduleend of module Prelude.Bool