Commit 2024-04-10 09:29 510ed4ef

feat: Ordinal Approximants of the least/greatest fixed point in a complete lattice (#8996) Define ordinal approximants for the least/greatest fixed points of a monotone function in a complete lattice. It is sometimes also called the constructive Knaster-Tarski Theorem, first introduced by Cousot & Cousot in 1979. This implementation is however not constructive. This has a variety of applications in non standard logics and proofs such as quantitative logics or cyclic proofs.