rzk-0.11.1: rzk.cabal
cabal-version: 2.0
-- This file has been generated from package.yaml by hpack version 0.39.1.
--
-- see: https://github.com/sol/hpack
name: rzk
version: 0.11.1
synopsis: An experimental proof assistant for synthetic ∞-categories
description: Please see the README on GitHub at <https://github.com/rzk-lang/rzk#readme>
category: Dependent Types
homepage: https://github.com/rzk-lang/rzk#readme
bug-reports: https://github.com/rzk-lang/rzk/issues
author: Nikolai Kudasov
maintainer: nickolay.kudasov@gmail.com
copyright: 2023-2025 Nikolai Kudasov
license: BSD3
license-file: LICENSE
build-type: Simple
extra-source-files:
grammar/Syntax.cf
test/typecheck/SCHEMA.md
test/typecheck/cases/happy-check.rzk
test/typecheck/cases/happy-data-bool.rzk
test/typecheck/cases/happy-data-circle.rzk
test/typecheck/cases/happy-data-coprod.rzk
test/typecheck/cases/happy-data-eliminator-reascription.rzk
test/typecheck/cases/happy-data-empty.rzk
test/typecheck/cases/happy-data-eta-short.rzk
test/typecheck/cases/happy-data-hit-reascription.rzk
test/typecheck/cases/happy-data-hottbook-nat.rzk
test/typecheck/cases/happy-data-indices-edge.rzk
test/typecheck/cases/happy-data-interval-funext.rzk
test/typecheck/cases/happy-data-large-warning.rzk
test/typecheck/cases/happy-data-list.rzk
test/typecheck/cases/happy-data-nat.rzk
test/typecheck/cases/happy-data-prop-trunc.rzk
test/typecheck/cases/happy-data-pushout.rzk
test/typecheck/cases/happy-data-rec-section.rzk
test/typecheck/cases/happy-data-section.rzk
test/typecheck/cases/happy-data-vec.rzk
test/typecheck/cases/happy-flip-unflip.rzk
test/typecheck/cases/happy-interval-basics.rzk
test/typecheck/cases/happy-interval-subtyping.rzk
test/typecheck/cases/happy-issue-9-relfunext2-id.rzk
test/typecheck/cases/happy-lattice-eq-gives-leq.rzk
test/typecheck/cases/happy-lattice-mixed-cube.rzk
test/typecheck/cases/happy-lattice.rzk
test/typecheck/cases/happy-match-basics.rzk
test/typecheck/cases/happy-match-case-vec.rzk
test/typecheck/cases/happy-match-indexed.rzk
test/typecheck/cases/happy-meta-prefix-option-off.rzk
test/typecheck/cases/happy-meta-prefix-plumbing.rzk
test/typecheck/cases/happy-modal-basics.rzk
test/typecheck/cases/happy-modal-flat-recOR-under-op.rzk
test/typecheck/cases/happy-modal-flat-under-op.rzk
test/typecheck/cases/happy-modal-inv.rzk
test/typecheck/cases/happy-modal-let-into.rzk
test/typecheck/cases/happy-modal-tope-unwrap.rzk
test/typecheck/cases/happy-modal-topes.rzk
test/typecheck/cases/happy-multivar-binder.rzk
test/typecheck/cases/happy-nbe-church-conversion.rzk
test/typecheck/cases/happy-op-hom-to-hom.rzk
test/typecheck/cases/happy-recbot-term-wellformed.rzk
test/typecheck/cases/happy-recor-guard-exceeds-context.rzk
test/typecheck/cases/happy-recor-split-simplex-overhang.rzk
test/typecheck/cases/happy-refl-path.rzk
test/typecheck/cases/happy-restrict-face-not-contained.rzk
test/typecheck/cases/happy-set-option-warn-overhang.rzk
test/typecheck/cases/happy-shadowing-across-groups.rzk
test/typecheck/cases/happy-shott-simplicial-subcomplexes.rzk
test/typecheck/cases/happy-subtype-variance-pi-shape-domain.rzk
test/typecheck/cases/happy-subtype-variance-restriction-faces.rzk
test/typecheck/cases/happy-subtype-variance-tope-family.rzk
test/typecheck/cases/happy-tope-high-dim-cubes.rzk
test/typecheck/cases/happy-tope-nested-rec-or-d4.rzk
test/typecheck/cases/happy-tope-nested-rec-or-d5.rzk
test/typecheck/cases/happy-tope-nested-rec-or-d6.rzk
test/typecheck/cases/happy-tope-nested-rec-or.rzk
test/typecheck/cases/happy-tope-rec-and-restrict.rzk
test/typecheck/cases/happy-tope-shapes.rzk
test/typecheck/cases/ill-bare-lambda-compute.rzk
test/typecheck/cases/ill-bare-refl-compute.rzk
test/typecheck/cases/ill-data-clash-generated.rzk
test/typecheck/cases/ill-data-compute-kind.rzk
test/typecheck/cases/ill-data-compute-mismatch.rzk
test/typecheck/cases/ill-data-compute-unknown.rzk
test/typecheck/cases/ill-data-duplicate-constructor.rzk
test/typecheck/cases/ill-data-eliminator-duplicate.rzk
test/typecheck/cases/ill-data-eliminator-mismatch.rzk
test/typecheck/cases/ill-data-eliminator-unknown.rzk
test/typecheck/cases/ill-data-fun-field.rzk
test/typecheck/cases/ill-data-index-mismatch.rzk
test/typecheck/cases/ill-data-missing-return.rzk
test/typecheck/cases/ill-data-negative.rzk
test/typecheck/cases/ill-data-non-u-sort.rzk
test/typecheck/cases/ill-data-path-endpoint.rzk
test/typecheck/cases/ill-data-path-higher-field.rzk
test/typecheck/cases/ill-data-path-higher.rzk
test/typecheck/cases/ill-data-path-indexed.rzk
test/typecheck/cases/ill-data-path-unannotated.rzk
test/typecheck/cases/ill-data-return-type.rzk
test/typecheck/cases/ill-data-shape-field.rzk
test/typecheck/cases/ill-duplicate.rzk
test/typecheck/cases/ill-hole-infer.rzk
test/typecheck/cases/ill-hole-pattern-binder-names.rzk
test/typecheck/cases/ill-hole-recor-branch.rzk
test/typecheck/cases/ill-hole-unsolved.rzk
test/typecheck/cases/ill-implicit.rzk
test/typecheck/cases/ill-interval-no-totality.rzk
test/typecheck/cases/ill-interval-subtyping.rzk
test/typecheck/cases/ill-invalid-arg-type-bot.rzk
test/typecheck/cases/ill-issue-13-flip-flip-wrong.rzk
test/typecheck/cases/ill-issue-206-families-of-extension.rzk
test/typecheck/cases/ill-issue-33-restriction-coherence.rzk
test/typecheck/cases/ill-lattice-endpoints-distinct.rzk
test/typecheck/cases/ill-lattice-eq-no-leak.rzk
test/typecheck/cases/ill-lattice-non-law.rzk
test/typecheck/cases/ill-lattice-not-interval-cube.rzk
test/typecheck/cases/ill-lattice-ops-glb-not-entailed.rzk
test/typecheck/cases/ill-lattice-ops-lub-not-entailed.rzk
test/typecheck/cases/ill-lattice-ops-lub-unconditional.rzk
test/typecheck/cases/ill-lattice-total-order-ii.rzk
test/typecheck/cases/ill-match-branch-arity.rzk
test/typecheck/cases/ill-match-cannot-infer.rzk
test/typecheck/cases/ill-match-duplicate-branch.rzk
test/typecheck/cases/ill-match-missing-branch.rzk
test/typecheck/cases/ill-match-missing-path-branch.rzk
test/typecheck/cases/ill-match-not-data.rzk
test/typecheck/cases/ill-match-unknown-branch.rzk
test/typecheck/cases/ill-modal-b-no-dist.rzk
test/typecheck/cases/ill-modal-flat-no-commute.rzk
test/typecheck/cases/ill-modal-let-into-body.rzk
test/typecheck/cases/ill-modal-not-modal.rzk
test/typecheck/cases/ill-modal-op-at-plain.rzk
test/typecheck/cases/ill-modal-op-under-flat.rzk
test/typecheck/cases/ill-modal-plain-under-flat.rzk
test/typecheck/cases/ill-modal-plain-under-op.rzk
test/typecheck/cases/ill-modal-recBOT-under-op-no-contradiction.rzk
test/typecheck/cases/ill-modal-sharp-at-plain.rzk
test/typecheck/cases/ill-modal-sharp-bot-not-bot.rzk
test/typecheck/cases/ill-modal-sharp-recOR-plain-var.rzk
test/typecheck/cases/ill-modal-sharp-under-flat.rzk
test/typecheck/cases/ill-modal-sharp-under-op.rzk
test/typecheck/cases/ill-modal-tope-cross-modality.rzk
test/typecheck/cases/ill-nbe-church-unequal.rzk
test/typecheck/cases/ill-not-function.rzk
test/typecheck/cases/ill-not-pair-first-unit.rzk
test/typecheck/cases/ill-not-pair-second-unit.rzk
test/typecheck/cases/ill-param-untyped-pattern.rzk
test/typecheck/cases/ill-rec-or-overlap-incoherent.rzk
test/typecheck/cases/ill-recbot-term-not-function.rzk
test/typecheck/cases/ill-recbot-term-undefined.rzk
test/typecheck/cases/ill-recor-as-tope.rzk
test/typecheck/cases/ill-recor-coverage-required.rzk
test/typecheck/cases/ill-recor-guard-disjoint.rzk
test/typecheck/cases/ill-render-latex-define.rzk
test/typecheck/cases/ill-repeated-binder-lambda.rzk
test/typecheck/cases/ill-repeated-binder-pair.rzk
test/typecheck/cases/ill-repeated-binder-params.rzk
test/typecheck/cases/ill-restrict-face-disjoint.rzk
test/typecheck/cases/ill-section-end-mismatch.rzk
test/typecheck/cases/ill-section-not-closed.rzk
test/typecheck/cases/ill-section-unexpected-end.rzk
test/typecheck/cases/ill-set-option-render.rzk
test/typecheck/cases/ill-set-option-unknown.rzk
test/typecheck/cases/ill-set-option-verbosity.rzk
test/typecheck/cases/ill-subtype-variance-pi-shape-domain.rzk
test/typecheck/cases/ill-subtype-variance-restriction-faces.rzk
test/typecheck/cases/ill-subtype-variance-tope-family.rzk
test/typecheck/cases/ill-tope-nested-rec-or-inner-singleton-d4.rzk
test/typecheck/cases/ill-tope-nested-rec-or-inner-singleton-d5.rzk
test/typecheck/cases/ill-tope-nested-rec-or-inner-singleton-d6.rzk
test/typecheck/cases/ill-tope-nested-rec-or-inner-singleton.rzk
test/typecheck/cases/ill-tope-not-satisfied-app-shape.rzk
test/typecheck/cases/ill-tope-not-satisfied-rec-bot.rzk
test/typecheck/cases/ill-tope-not-satisfied-rec-or-boundary-equiv.rzk
test/typecheck/cases/ill-tope-not-satisfied-rec-or-open-singleton.rzk
test/typecheck/cases/ill-tope-not-satisfied-tope-family-subtyping.rzk
test/typecheck/cases/ill-tope-param-lambda.rzk
test/typecheck/cases/ill-tope-param-typefun.rzk
test/typecheck/cases/ill-tope-pattern-binder-bare.rzk
test/typecheck/cases/ill-tope-recOR-non-discrete.rzk
test/typecheck/cases/ill-tope-subtle-app-shape-5d.rzk
test/typecheck/cases/ill-tope-subtle-rec-or-5d-boundary.rzk
test/typecheck/cases/ill-tope-subtle-tope-family-4d.rzk
test/typecheck/cases/ill-tope-subtle-tope-family-5d.rzk
test/typecheck/cases/ill-undefined.rzk
test/typecheck/cases/ill-unexpected-lambda.rzk
test/typecheck/cases/ill-unexpected-pair.rzk
test/typecheck/cases/ill-unexpected-refl.rzk
test/typecheck/cases/ill-unify-id-free-path.rzk
test/typecheck/cases/ill-unify-terms-path.rzk
test/typecheck/cases/ill-unify.rzk
test/typecheck/cases/ill-unset-option-unknown.rzk
test/typecheck/cases/ill-unused-assumption.rzk
test/typecheck/cases/multimodule-first-error/bad.rzk
test/typecheck/cases/multimodule-first-error/lib.rzk
test/typecheck/cases/multimodule-two-ok/lib.rzk
test/typecheck/cases/multimodule-two-ok/user.rzk
test/typecheck/cases/uses-whnf-discarded.rzk
test/typecheck/cases/uses-whnf-masked-transitive.rzk
test/typecheck/cases/warn-meta-prefix-object-position.rzk
test/typecheck/cases/warn-meta-prefix-option-structural.rzk
test/typecheck/cases/warn-meta-prefix-section.rzk
test/typecheck/cases/warn-meta-prefix-strict-only.rzk
test/typecheck/cases/happy-check.expect.yaml
test/typecheck/cases/happy-data-bool.expect.yaml
test/typecheck/cases/happy-data-circle.expect.yaml
test/typecheck/cases/happy-data-coprod.expect.yaml
test/typecheck/cases/happy-data-eliminator-reascription.expect.yaml
test/typecheck/cases/happy-data-empty.expect.yaml
test/typecheck/cases/happy-data-eta-short.expect.yaml
test/typecheck/cases/happy-data-hit-reascription.expect.yaml
test/typecheck/cases/happy-data-hottbook-nat.expect.yaml
test/typecheck/cases/happy-data-indices-edge.expect.yaml
test/typecheck/cases/happy-data-interval-funext.expect.yaml
test/typecheck/cases/happy-data-large-warning.expect.yaml
test/typecheck/cases/happy-data-list.expect.yaml
test/typecheck/cases/happy-data-nat.expect.yaml
test/typecheck/cases/happy-data-prop-trunc.expect.yaml
test/typecheck/cases/happy-data-pushout.expect.yaml
test/typecheck/cases/happy-data-rec-section.expect.yaml
test/typecheck/cases/happy-data-section.expect.yaml
test/typecheck/cases/happy-data-vec.expect.yaml
test/typecheck/cases/happy-flip-unflip.expect.yaml
test/typecheck/cases/happy-interval-basics.expect.yaml
test/typecheck/cases/happy-interval-subtyping.expect.yaml
test/typecheck/cases/happy-issue-9-relfunext2-id.expect.yaml
test/typecheck/cases/happy-lattice-eq-gives-leq.expect.yaml
test/typecheck/cases/happy-lattice-mixed-cube.expect.yaml
test/typecheck/cases/happy-lattice.expect.yaml
test/typecheck/cases/happy-match-basics.expect.yaml
test/typecheck/cases/happy-match-case-vec.expect.yaml
test/typecheck/cases/happy-match-indexed.expect.yaml
test/typecheck/cases/happy-meta-prefix-option-off.expect.yaml
test/typecheck/cases/happy-meta-prefix-plumbing.expect.yaml
test/typecheck/cases/happy-modal-basics.expect.yaml
test/typecheck/cases/happy-modal-flat-recOR-under-op.expect.yaml
test/typecheck/cases/happy-modal-flat-under-op.expect.yaml
test/typecheck/cases/happy-modal-inv.expect.yaml
test/typecheck/cases/happy-modal-let-into.expect.yaml
test/typecheck/cases/happy-modal-tope-unwrap.expect.yaml
test/typecheck/cases/happy-modal-topes.expect.yaml
test/typecheck/cases/happy-multivar-binder.expect.yaml
test/typecheck/cases/happy-nbe-church-conversion.expect.yaml
test/typecheck/cases/happy-op-hom-to-hom.expect.yaml
test/typecheck/cases/happy-recbot-term-wellformed.expect.yaml
test/typecheck/cases/happy-recor-guard-exceeds-context.expect.yaml
test/typecheck/cases/happy-recor-split-simplex-overhang.expect.yaml
test/typecheck/cases/happy-refl-path.expect.yaml
test/typecheck/cases/happy-restrict-face-not-contained.expect.yaml
test/typecheck/cases/happy-set-option-warn-overhang.expect.yaml
test/typecheck/cases/happy-shadowing-across-groups.expect.yaml
test/typecheck/cases/happy-shott-simplicial-subcomplexes.expect.yaml
test/typecheck/cases/happy-subtype-variance-pi-shape-domain.expect.yaml
test/typecheck/cases/happy-subtype-variance-restriction-faces.expect.yaml
test/typecheck/cases/happy-subtype-variance-tope-family.expect.yaml
test/typecheck/cases/happy-tope-high-dim-cubes.expect.yaml
test/typecheck/cases/happy-tope-nested-rec-or-d4.expect.yaml
test/typecheck/cases/happy-tope-nested-rec-or-d5.expect.yaml
test/typecheck/cases/happy-tope-nested-rec-or-d6.expect.yaml
test/typecheck/cases/happy-tope-nested-rec-or.expect.yaml
test/typecheck/cases/happy-tope-rec-and-restrict.expect.yaml
test/typecheck/cases/happy-tope-shapes.expect.yaml
test/typecheck/cases/ill-bare-lambda-compute.expect.yaml
test/typecheck/cases/ill-bare-refl-compute.expect.yaml
test/typecheck/cases/ill-data-clash-generated.expect.yaml
test/typecheck/cases/ill-data-compute-kind.expect.yaml
test/typecheck/cases/ill-data-compute-mismatch.expect.yaml
test/typecheck/cases/ill-data-compute-unknown.expect.yaml
test/typecheck/cases/ill-data-duplicate-constructor.expect.yaml
test/typecheck/cases/ill-data-eliminator-duplicate.expect.yaml
test/typecheck/cases/ill-data-eliminator-mismatch.expect.yaml
test/typecheck/cases/ill-data-eliminator-unknown.expect.yaml
test/typecheck/cases/ill-data-fun-field.expect.yaml
test/typecheck/cases/ill-data-index-mismatch.expect.yaml
test/typecheck/cases/ill-data-missing-return.expect.yaml
test/typecheck/cases/ill-data-negative.expect.yaml
test/typecheck/cases/ill-data-non-u-sort.expect.yaml
test/typecheck/cases/ill-data-path-endpoint.expect.yaml
test/typecheck/cases/ill-data-path-higher-field.expect.yaml
test/typecheck/cases/ill-data-path-higher.expect.yaml
test/typecheck/cases/ill-data-path-indexed.expect.yaml
test/typecheck/cases/ill-data-path-unannotated.expect.yaml
test/typecheck/cases/ill-data-return-type.expect.yaml
test/typecheck/cases/ill-data-shape-field.expect.yaml
test/typecheck/cases/ill-duplicate.expect.yaml
test/typecheck/cases/ill-hole-infer.expect.yaml
test/typecheck/cases/ill-hole-pattern-binder-names.expect.yaml
test/typecheck/cases/ill-hole-recor-branch.expect.yaml
test/typecheck/cases/ill-hole-unsolved.expect.yaml
test/typecheck/cases/ill-implicit.expect.yaml
test/typecheck/cases/ill-interval-no-totality.expect.yaml
test/typecheck/cases/ill-interval-subtyping.expect.yaml
test/typecheck/cases/ill-invalid-arg-type-bot.expect.yaml
test/typecheck/cases/ill-issue-13-flip-flip-wrong.expect.yaml
test/typecheck/cases/ill-issue-206-families-of-extension.expect.yaml
test/typecheck/cases/ill-issue-33-restriction-coherence.expect.yaml
test/typecheck/cases/ill-lattice-endpoints-distinct.expect.yaml
test/typecheck/cases/ill-lattice-eq-no-leak.expect.yaml
test/typecheck/cases/ill-lattice-non-law.expect.yaml
test/typecheck/cases/ill-lattice-not-interval-cube.expect.yaml
test/typecheck/cases/ill-lattice-ops-glb-not-entailed.expect.yaml
test/typecheck/cases/ill-lattice-ops-lub-not-entailed.expect.yaml
test/typecheck/cases/ill-lattice-ops-lub-unconditional.expect.yaml
test/typecheck/cases/ill-lattice-total-order-ii.expect.yaml
test/typecheck/cases/ill-match-branch-arity.expect.yaml
test/typecheck/cases/ill-match-cannot-infer.expect.yaml
test/typecheck/cases/ill-match-duplicate-branch.expect.yaml
test/typecheck/cases/ill-match-missing-branch.expect.yaml
test/typecheck/cases/ill-match-missing-path-branch.expect.yaml
test/typecheck/cases/ill-match-not-data.expect.yaml
test/typecheck/cases/ill-match-unknown-branch.expect.yaml
test/typecheck/cases/ill-modal-b-no-dist.expect.yaml
test/typecheck/cases/ill-modal-flat-no-commute.expect.yaml
test/typecheck/cases/ill-modal-let-into-body.expect.yaml
test/typecheck/cases/ill-modal-not-modal.expect.yaml
test/typecheck/cases/ill-modal-op-at-plain.expect.yaml
test/typecheck/cases/ill-modal-op-under-flat.expect.yaml
test/typecheck/cases/ill-modal-plain-under-flat.expect.yaml
test/typecheck/cases/ill-modal-plain-under-op.expect.yaml
test/typecheck/cases/ill-modal-recBOT-under-op-no-contradiction.expect.yaml
test/typecheck/cases/ill-modal-sharp-at-plain.expect.yaml
test/typecheck/cases/ill-modal-sharp-bot-not-bot.expect.yaml
test/typecheck/cases/ill-modal-sharp-recOR-plain-var.expect.yaml
test/typecheck/cases/ill-modal-sharp-under-flat.expect.yaml
test/typecheck/cases/ill-modal-sharp-under-op.expect.yaml
test/typecheck/cases/ill-modal-tope-cross-modality.expect.yaml
test/typecheck/cases/ill-nbe-church-unequal.expect.yaml
test/typecheck/cases/ill-not-function.expect.yaml
test/typecheck/cases/ill-not-pair-first-unit.expect.yaml
test/typecheck/cases/ill-not-pair-second-unit.expect.yaml
test/typecheck/cases/ill-param-untyped-pattern.expect.yaml
test/typecheck/cases/ill-rec-or-overlap-incoherent.expect.yaml
test/typecheck/cases/ill-recbot-term-not-function.expect.yaml
test/typecheck/cases/ill-recbot-term-undefined.expect.yaml
test/typecheck/cases/ill-recor-as-tope.expect.yaml
test/typecheck/cases/ill-recor-coverage-required.expect.yaml
test/typecheck/cases/ill-recor-guard-disjoint.expect.yaml
test/typecheck/cases/ill-render-latex-define.expect.yaml
test/typecheck/cases/ill-repeated-binder-lambda.expect.yaml
test/typecheck/cases/ill-repeated-binder-pair.expect.yaml
test/typecheck/cases/ill-repeated-binder-params.expect.yaml
test/typecheck/cases/ill-restrict-face-disjoint.expect.yaml
test/typecheck/cases/ill-section-end-mismatch.expect.yaml
test/typecheck/cases/ill-section-not-closed.expect.yaml
test/typecheck/cases/ill-section-unexpected-end.expect.yaml
test/typecheck/cases/ill-set-option-render.expect.yaml
test/typecheck/cases/ill-set-option-unknown.expect.yaml
test/typecheck/cases/ill-set-option-verbosity.expect.yaml
test/typecheck/cases/ill-subtype-variance-pi-shape-domain.expect.yaml
test/typecheck/cases/ill-subtype-variance-restriction-faces.expect.yaml
test/typecheck/cases/ill-subtype-variance-tope-family.expect.yaml
test/typecheck/cases/ill-tope-nested-rec-or-inner-singleton-d4.expect.yaml
test/typecheck/cases/ill-tope-nested-rec-or-inner-singleton-d5.expect.yaml
test/typecheck/cases/ill-tope-nested-rec-or-inner-singleton-d6.expect.yaml
test/typecheck/cases/ill-tope-nested-rec-or-inner-singleton.expect.yaml
test/typecheck/cases/ill-tope-not-satisfied-app-shape.expect.yaml
test/typecheck/cases/ill-tope-not-satisfied-rec-bot.expect.yaml
test/typecheck/cases/ill-tope-not-satisfied-rec-or-boundary-equiv.expect.yaml
test/typecheck/cases/ill-tope-not-satisfied-rec-or-open-singleton.expect.yaml
test/typecheck/cases/ill-tope-not-satisfied-tope-family-subtyping.expect.yaml
test/typecheck/cases/ill-tope-param-lambda.expect.yaml
test/typecheck/cases/ill-tope-param-typefun.expect.yaml
test/typecheck/cases/ill-tope-pattern-binder-bare.expect.yaml
test/typecheck/cases/ill-tope-recOR-non-discrete.expect.yaml
test/typecheck/cases/ill-tope-subtle-app-shape-5d.expect.yaml
test/typecheck/cases/ill-tope-subtle-rec-or-5d-boundary.expect.yaml
test/typecheck/cases/ill-tope-subtle-tope-family-4d.expect.yaml
test/typecheck/cases/ill-tope-subtle-tope-family-5d.expect.yaml
test/typecheck/cases/ill-undefined.expect.yaml
test/typecheck/cases/ill-unexpected-lambda.expect.yaml
test/typecheck/cases/ill-unexpected-pair.expect.yaml
test/typecheck/cases/ill-unexpected-refl.expect.yaml
test/typecheck/cases/ill-unify-id-free-path.expect.yaml
test/typecheck/cases/ill-unify-terms-path.expect.yaml
test/typecheck/cases/ill-unify.expect.yaml
test/typecheck/cases/ill-unset-option-unknown.expect.yaml
test/typecheck/cases/ill-unused-assumption.expect.yaml
test/typecheck/cases/uses-whnf-discarded.expect.yaml
test/typecheck/cases/uses-whnf-masked-transitive.expect.yaml
test/typecheck/cases/warn-meta-prefix-object-position.expect.yaml
test/typecheck/cases/warn-meta-prefix-option-structural.expect.yaml
test/typecheck/cases/warn-meta-prefix-section.expect.yaml
test/typecheck/cases/warn-meta-prefix-strict-only.expect.yaml
test/typecheck/cases/literate-fence/expect.yaml
test/typecheck/cases/multimodule-first-error/expect.yaml
test/typecheck/cases/multimodule-two-ok/expect.yaml
test/typecheck/cases/literate-fence/doc.rzk.md
extra-doc-files:
README.md
ChangeLog.md
source-repository head
type: git
location: https://github.com/rzk-lang/rzk
flag lsp
description: Build with LSP support (only available with GHC, not GHCJS).
manual: True
default: True
library
exposed-modules:
Language.Rzk.Foil.Convert
Language.Rzk.Foil.Names
Language.Rzk.Foil.Print
Language.Rzk.Foil.Syntax
Language.Rzk.Syntax
Language.Rzk.Syntax.Abs
Language.Rzk.Syntax.Layout
Language.Rzk.Syntax.Lex
Language.Rzk.Syntax.Par
Language.Rzk.Syntax.Print
Rzk
Rzk.Diagnostic
Rzk.Format
Rzk.Main
Rzk.Project.Config
Rzk.Render.Geometry
Rzk.TypeCheck
Rzk.TypeCheck.BinderTypes
Rzk.TypeCheck.Context
Rzk.TypeCheck.Decl
Rzk.TypeCheck.Decl.Data
Rzk.TypeCheck.Display
Rzk.TypeCheck.Error
Rzk.TypeCheck.Eval
Rzk.TypeCheck.Judgements
Rzk.TypeCheck.MetaPrefix
Rzk.TypeCheck.Monad
Rzk.TypeCheck.NbE
Rzk.TypeCheck.Render
Rzk.TypeCheck.Unify
other-modules:
Paths_rzk
autogen-modules:
Paths_rzk
hs-source-dirs:
src
default-extensions:
DeriveDataTypeable
ghc-options: -Wall -Wcompat -Widentities -Werror=missing-fields -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path
build-depends:
Glob >=0.9.3 && <1
, aeson >=1.4 && <3
, array >=0.5.3.0 && <1
, base >=4.7 && <5
, bifunctors >=5.5.3 && <6
, bytestring >=0.10.8.2 && <1
, containers >=0.6 && <1
, directory >=1.2.7.0 && <2
, free-foil >=0.3.2 && <0.4
, kind-generics >=0.5 && <1
, kind-generics-th >=0.2 && <1
, mtl >=2.2.2 && <3
, template-haskell >=2.14.0.0 && <3
, text >=1.2.3.1 && <3
, transformers >=0.5 && <1
, yaml >=0.11.0.0 && <1
default-language: Haskell2010
if flag(lsp) && !impl(ghcjs)
cpp-options: -DLSP_ENABLED
if flag(lsp) && !impl(ghcjs)
exposed-modules:
Language.Rzk.VSCode.Config
Language.Rzk.VSCode.Env
Language.Rzk.VSCode.Handlers
Language.Rzk.VSCode.Logging
Language.Rzk.VSCode.Lsp
Language.Rzk.VSCode.PositionEncoding
Language.Rzk.VSCode.Tokenize
Language.Rzk.VSCode.ReferenceIndex
build-depends:
aeson >=2.0.0.0 && <3
, async >=2.2 && <3
, co-log-core >=0.3.2.0 && <1
, data-default-class >=0.1.2.0 && <1
, filepath >=1.4.100.0 && <2
, lens >=5.0.1 && <6
, lsp >=2.4.0.0 && <3
, lsp-types >=2.1.1.0 && <3
, mtl >=2.3.1 && <3
, stm >=2.5.1.0 && <3
executable rzk
main-is: Main.hs
other-modules:
Paths_rzk
autogen-modules:
Paths_rzk
hs-source-dirs:
app
default-extensions:
DeriveDataTypeable
ghc-options: -Wall -Wcompat -Widentities -Werror=missing-fields -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -threaded -rtsopts "-with-rtsopts=-N -A64m"
build-depends:
Glob >=0.9.3 && <1
, aeson >=1.4 && <3
, array >=0.5.3.0 && <1
, base >=4.7 && <5
, bifunctors >=5.5.3 && <6
, bytestring >=0.10.8.2 && <1
, containers >=0.6 && <1
, directory >=1.2.7.0 && <2
, free-foil >=0.3.2 && <0.4
, kind-generics >=0.5 && <1
, kind-generics-th >=0.2 && <1
, mtl >=2.2.2 && <3
, rzk
, template-haskell >=2.14.0.0 && <3
, text >=1.2.3.1 && <3
, transformers >=0.5 && <1
, yaml >=0.11.0.0 && <1
default-language: Haskell2010
if flag(lsp) && !impl(ghcjs)
cpp-options: -DLSP_ENABLED
if !impl(ghcjs)
build-depends:
optparse-generic >=1.4.7 && <2
, with-utf8 >=1.0.3.0 && <2
test-suite doctests
type: exitcode-stdio-1.0
main-is: doctests.hs
hs-source-dirs:
test
default-extensions:
DeriveDataTypeable
ghc-options: -Wall -Wcompat -Widentities -Werror=missing-fields -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path
build-depends:
Glob >=0.9.3 && <1
, QuickCheck >=2.14 && <3
, aeson >=1.4 && <3
, array >=0.5.3.0 && <1
, base >=4.11.0.0 && <5.0
, bifunctors >=5.5.3 && <6
, bytestring >=0.10.8.2 && <1
, containers >=0.6 && <1
, directory >=1.2.7.0 && <2
, doctest-parallel >=0.3 && <1
, free-foil >=0.3.2 && <0.4
, kind-generics >=0.5 && <1
, kind-generics-th >=0.2 && <1
, mtl >=2.2.2 && <3
, rzk
, template-haskell >=2.14.0.0 && <3
, text >=1.2.3.1 && <3
, transformers >=0.5 && <1
, yaml >=0.11.0.0 && <1
default-language: Haskell2010
if flag(lsp) && !impl(ghcjs)
cpp-options: -DLSP_ENABLED
test-suite rzk-test
type: exitcode-stdio-1.0
main-is: Spec.hs
other-modules:
Rzk.BinderTypesSpec
Rzk.DiagnosticSpec
Rzk.FoilCoreSpec
Rzk.FormatSpec
Rzk.HolesSpec
Rzk.ParserSpec
Rzk.PositionEncodingSpec
Rzk.RefIndexSpec
Rzk.SemanticTokensSpec
Rzk.TypeCheckSpec
Paths_rzk
autogen-modules:
Paths_rzk
hs-source-dirs:
test
default-extensions:
DeriveDataTypeable
ghc-options: -Wall -Wcompat -Widentities -Werror=missing-fields -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -threaded -rtsopts -with-rtsopts=-N
build-tool-depends:
hspec-discover:hspec-discover >=2.7 && <3
build-depends:
Glob >=0.9.3 && <1
, aeson >=1.4 && <3
, array >=0.5.3.0 && <1
, base >=4.7 && <5
, bifunctors >=5.5.3 && <6
, bytestring >=0.10.8.2 && <1
, containers >=0.6 && <1
, directory >=1.2.7.0 && <2
, filepath >=1.4 && <2
, free-foil >=0.3.2 && <0.4
, hspec >=2.7 && <3
, hspec-discover >=2.7 && <3
, kind-generics >=0.5 && <1
, kind-generics-th >=0.2 && <1
, mtl >=2.2.2 && <3
, rzk
, template-haskell >=2.14.0.0 && <3
, text >=1.2.3.1 && <3
, transformers >=0.5 && <1
, yaml >=0.11.0.0 && <1
default-language: Haskell2010
if flag(lsp) && !impl(ghcjs)
cpp-options: -DLSP_ENABLED
if flag(lsp) && !impl(ghcjs)
build-depends:
lsp-types >=2.1.1.0 && <3