package beluga

You can search for identifiers within the package.

in-package search v0.2.0

Implementation of contextual modal logic for reasoning with higher-order abstract syntax

Install

sha256=a6b4e3b3b51cd4cb5575b6f5cf7da88aa37027e273925752a50a3f7c97f0ed8c

sha512=070d2ee1f67583bf0619d4209369234a9ee948145b674c2a6b05586e96f5a45b2b73cadea0c67958e4ed03eb72e9ca72a037758a4db0d7e7d57eb1a3a98efc9c

Parsing and disambiguation of non-normal expressions is supported.
Parsing of prefix, infix and postfix operators is supported for computation-level type family constants and constructors, as well as type-annotated programs and values.
Improved error-reporting with printing of source code.
Pretty-printing of Beluga signatures to HTML now supports hyperlinks for constants to their declaration site.

Substitution meta-objects need to be prefixed by $. That is, the plain substitution [g |- $S] must be written as $[g |- $S], and the renaming substitution [g |-# $S] must be written as $[g |-# $S].
Substitution meta-types need to be prefixed by $. That is, the plain substitution meta-type [g |- h] must be written as $[g |- h], and the renaming substitution meta-type [g |-# h] must be written as $[g |-# h].
Parameter types need to be prefixed by #. That is, {#p : [g |- nat]} must be written as {#p : #[g |- nat]}.
Identifier overloading is disallowed. This means that term-level constants may not be overloaded with type-level constants.
Freezing of type family declarations is more strict. This means that old-style LF term-level constants cannot be added to type families after any declaration other than old-style LF type or term-level constant declarations.
Destructors for coinductive type families use postfix notation, like projections or field accesses (i.e., s .hd, s .tl). This applies both in computation-level patterns and expressions.
Namespaces are now fully supported in Beluga signatures.

Interactive Harpoon sessions are now local to the referencing environment in which they are declared.
Lexing of nested delimited comments %{{, }}% and %{, }% is fixed.
--open pragmas behave like OCaml's open directive, whereby declarations introduced by --open are not re-exported, and not copy/pasted textually.