Nuprl Definition : iff-type-lattice
iff-type-lattice{i:l}() == mk-bounded-lattice(PType;λ2A B.p-and(A;B);λ2A B.p-or(A;B);False;True)
Definitions occuring in Statement :
p-or: p-or(A;B),
p-and: p-and(A;B),
p-type: PType,
mk-bounded-lattice: mk-bounded-lattice(T;m;j;z;o),
so_lambda: λ2x y.t[x; y],
false: False,
true: True
Definitions occuring in definition :
mk-bounded-lattice: mk-bounded-lattice(T;m;j;z;o),
p-type: PType,
p-and: p-and(A;B),
so_lambda: λ2x y.t[x; y],
p-or: p-or(A;B),
false: False,
true: True
FDL editor aliases :
iff-type-lattice
Latex:
iff-type-lattice\{i:l\}() == mk-bounded-lattice(PType;\mlambda{}\msubtwo{}A B.p-and(A;B);\mlambda{}\msubtwo{}A B.p-or(A;B);False;True)
Date html generated:
2020_05_20-AM-08_24_48
Last ObjectModification:
2018_10_15-PM-01_30_33
Theory : lattices
Home
Index