Nuprl Definition : type-lattice
type-lattice{i:l}() == mk-bounded-lattice(EType;λ2A B.e-isect(A;B);λ2A B.e-union(A;B);Void;Top)
Definitions occuring in Statement :
e-union: e-union(A;B),
e-isect: e-isect(A;B),
e-type: EType,
mk-bounded-lattice: mk-bounded-lattice(T;m;j;z;o),
top: Top,
so_lambda: λ2x y.t[x; y],
void: Void
Definitions occuring in definition :
mk-bounded-lattice: mk-bounded-lattice(T;m;j;z;o),
e-type: EType,
e-isect: e-isect(A;B),
so_lambda: λ2x y.t[x; y],
e-union: e-union(A;B),
void: Void,
top: Top
FDL editor aliases :
type-lattice
Latex:
type-lattice\{i:l\}() == mk-bounded-lattice(EType;\mlambda{}\msubtwo{}A B.e-isect(A;B);\mlambda{}\msubtwo{}A B.e-union(A;B);Void;Top)
Date html generated:
2019_10_31-AM-07_20_08
Last ObjectModification:
2018_10_12-PM-00_39_02
Theory : lattices
Home
Index