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.