rzk 0.5 → 0.5.1

raw patch · 3 files changed

+17/−1 lines, 3 files

Files

• ChangeLog.md +11/−0
• rzk.cabal +1/−1
• src/Rzk/TypeCheck.hs +5/−0

@@ -6,6 +6,17 @@ and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). +## v0.5.1 — 2022-06-29++This version fixes `Unit` type and makes some changes to documentation:++- Fix computation for `Unit` (see [2f7d6295]( https://github.com/fizruk/rzk/commit/2f7d6295 ));+- Update documentation (see [ea2d176b]( https://github.com/fizruk/rzk/commit/ea2d176b ));+- Use mike to deploy versioned docs (see [99cf721a]( https://github.com/fizruk/rzk/commit/99cf721a ));+- Replace MkDocs hook with the published plugin (see [#58]( https://github.com/fizruk/rzk/pull/58 ));+- Switch to Material theme for MkDocs (see [#57]( https://github.com/fizruk/rzk/pull/57 ));+- Fix links to `*.rzk.md` in `mkdocs.yml` (see [8ba1c55b]( https://github.com/fizruk/rzk/commit/8ba1c55b ));+ ## v0.5 — 2022-06-20  This version contains the following changes:

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           rzk-version:        0.5+version:        0.5.1 synopsis:       An experimental proof assistant for synthetic ∞-categories description:    Please see the README on GitHub at <https://github.com/fizruk/rzk#readme> category:       Dependent Types

@@ -1257,6 +1257,11 @@     UniverseCubeT{} -> nfTope tt     UniverseTopeT{} -> nfTope tt +    -- CubeUnitT{} -> pure cubeUnitStarT -- compute an expression of 1 cube to its only point+    TypeUnitT{} -> pure unitT -- compute an expression of Unit type to unit+    -- FIXME: next line is ad hoc, should be improved!+    TypeRestrictedT _info TypeUnitT{} _rs -> pure unitT -- compute an expression of Unit type to unit+     -- check if we have cube point term (if so, compute NF)     typeOf_tt -> typeOf typeOf_tt >>= \case       UniverseCubeT{} -> nfTope tt