monsterkrampePossiblyInfiniteTrees0.1.0

This repo formalizes (possibly) infinite trees of finite degree in Lean. So far this is mainly a dependency for one of my other projects and tailored towards this purpose. The repo features a formalization of (a special case of) König's Lemma.
Displaying 1-1 of 1 packages depending on monsterkrampe/PossiblyInfiniteTrees
Sort by

  1. monsterkrampe/ExistentialRulesuses4a9276e

    This repo contains formalizations around Existential Rules (aka. Tuple-Generating Dependencies) with disjunctions and the Chase algorithm. Mostly this will be about (basics of) my own formal works.