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).