Computational realization of filters (experimental) #
This file provides infrastructure to compute with filters.
Main declarations #
- f : σ → α
- pt : σ
- inf : σ → σ → σ
- inf_le_left : ∀ (a b : σ), CFilter.f s (CFilter.inf s a b) ≤ CFilter.f s a
- inf_le_right : ∀ (a b : σ), CFilter.f s (CFilter.inf s a b) ≤ CFilter.f s b
A CFilter α σ
is a realization of a filter (base) on α
,
represented by a type σ
together with operations for the top element and
the binary inf
operation.
Instances For
Map a CFilter
to an equivalent representation type.
Instances For
Transfer a realizer along an equality of filter. This has better definitional equalities than
the Eq.rec
proof.
Instances For
A filter realizes itself.
Instances For
Transfer a filter realizer to another realizer on a different base type.
Instances For
Unit
is a realizer for the principal filter
Instances For
Unit
is a realizer for the top filter
Instances For
Unit
is a realizer for the bottom filter
Instances For
Construct a realizer for map m f
given a realizer for f
Instances For
Construct a realizer for comap m f
given a realizer for f
Instances For
Construct a realizer for the sup of two filters
Instances For
Construct a realizer for the inf of two filters
Instances For
Construct a realizer for the cofinite filter
Instances For
Construct a realizer for filter bind
Instances For
Construct a realizer for indexed supremum
Instances For
Construct a realizer for the product of filters