Tags: ppolesiuk/IxFree
Tags
Version 1.1.0 (#2) The new version of IxFree (1.1.0) introduces the following features and improvements. - Definition and notation of strict preorder on worlds `w ⊏↓ w'`, i.e., when step index is strictly lower. - Later-distribution laws for connectives; - `IWorldLift` and `IWorldUnlift` typeclasses that provide operation of lifting and unlifting a step-index of given world. This optional structure of worlds is required for some later-distribution laws. - `IWorldBottomDec` class that expresses decidability of the existence of a future world with lower step index. - `index_case` tactic that provides inference rule for case analysis on the existence of a world described by `IWorldBottomDec` class. - Instances of new classes for `Nat` worlds. - Löb induction was moved to other module `LaterRules`, that contains other properties of later modality (distribution laws, index case analysis, etc.).