Skip to content

Tags: ppolesiuk/IxFree

Tags

1.1.0

Toggle 1.1.0's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
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.).

1.0.0

Toggle 1.0.0's commit message
Version 1.0.0