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=a1feed16ff859a47859a73b89f751911744f1ed427c6dfd24466d0f817a9fa6b

sha512=a6dcddfc74a8abdf0578ad249fa7fda52168ec7d991784236dbac3ac331777bf3a14d8fc205c8c2b734409eabc008966276a5683c51449322122a3f52c69e96e

Updated the Beluga mode for Emacs to use the 'cl-lib library instead of 'cl.

Colouring of error messages is fixed for the Beluga mode for Emacs using the 'ansi-color library (requires Emacs >= v28.1).

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.