Legacy Syntax

Beluga is major research project, constantly undergoing development. Over the years we've made many changes to the language's syntax. We've outlined some of the obsolete syntax you may encounter in older publications.

Year Release Old Syntax New Syntax Expression
2008 0.1 box(g. x) [g |- x] Contextual object where g : context variable, x : variable bound in g
2008 0.1 all A:t {A:t} Universal quantification where A : meta-variable, t : type
2008 0.1 M[id, x] M .. x Delayed substitution where M : meta-variable, .., id : identity substitution, x : bound variable
2008 0.1 ctx schema gCtx schema gCtx Schema declaration where gCtx : schema identifier
2010 0.3 (obj T)[g] [g |- obj T] Contextual object where g : context variable, obj : LF constructor, T : meta-variable
2010 0.3 {g:(ctx)*} {g: ctx} Universal quantification where g : context variable, ctx : schema
2012 0.5 [g. obj T] [g |- obj T] Contextual object where g : context variable, obj : LF constructor, T : meta-variable
2014 0.5 {#S:g[h]} {#S: [h |- g]} Universal quantification where #S : substitution variable, g : domain, h : range
2014 0.5 #S[] #S[^] Empty subst. closure where #S : substitution variable
2015 0.8.2 [g |- M ..] [g |- M[..]] Meta-variables are associated with explicit substitutions
2015 0.8.2 [g |- M[..]] [g |- M] Meta-variables are associated with explicit substitutions; they can be omitted as long as they are identity substitutions
2015 0.8.2 [g |- M ] [g |- M[^]] Meta-variables are associated with explicit substitutions; they must now be associated with a weakening substitution indicating M is closed
2015 0.8.2 datatype tm : type = ... LF tm : type = ... Distinguish between LF, inductive, and stratified data types.
2015 0.8.2 datatype Tm : ctype = ... inductive Tm : ctype = ... Distinguish between LF, inductive, and stratified data types.
2015 0.8.2 datatype Tm : ctype = ... stratified Tm : [|- tp] -> ctype = ... Distinguish between LF, inductive, and stratified data types.
2018 0.8.2 %{coverage, warncoverage,
nostrengthen, infix, prefix, assoc,
name, abbrev, not, open} ...		 --{coverage, warncoverage,
nostrengthen, infix, prefix, assoc,
name, abbrev, not, open} ...		 Pragmas use -- instead of % (different syntax for pragmas and comments)
2023 1.1 $σ' : [g |- $σ, M] $σ' : $[g |- $σ, M] Substitution types and objects require a $ prefix.
2023 1.1 $σ' : [g |-# $σ, M] $σ' : $[g |-# $σ, M] Renaming substitution types and objects require a $ prefix.
2023 1.1 #p : [g |- tp] #p : #[g |- tp] Parameter types and variables require a # prefix.
2023 1.1 tl stream stream .tl Destructors for coinductive type families use postfix notation.

© Computation and Logic Group McGill University Logo
Department of Computer Science, McGill University
3480 University Street, Montreal, Quebec, Canada, H3A 0E9