Nuprl Definition : free-dl
free-dl(X) == {points=free-dl-type(X);meet=λ2x y.free-dl-meet(x;y);join=λ2x y.free-dl-join(x;y);0=[];1=[[]]}
Definitions occuring in Statement :
free-dl-meet: free-dl-meet(as;bs),
free-dl-join: free-dl-join(as;bs),
free-dl-type: free-dl-type(X),
mk-bounded-distributive-lattice: mk-bounded-distributive-lattice,
cons: [a / b],
nil: [],
so_lambda: λ2x y.t[x; y]
Definitions occuring in definition :
mk-bounded-distributive-lattice: mk-bounded-distributive-lattice,
free-dl-type: free-dl-type(X),
free-dl-meet: free-dl-meet(as;bs),
so_lambda: λ2x y.t[x; y],
free-dl-join: free-dl-join(as;bs),
cons: [a / b],
nil: []
FDL editor aliases :
free-dl
Latex:
free-dl(X) ==
\{points=free-dl-type(X);
meet=\mlambda{}\msubtwo{}x y.free-dl-meet(x;y);
join=\mlambda{}\msubtwo{}x y.free-dl-join(x;y);
0=[];
1=[[]]\}
Date html generated:
2020_05_20-AM-08_27_08
Last ObjectModification:
2017_01_21-PM-05_36_09
Theory : lattices
Home
Index