Syntax of terms
The BNF grammar of Lambdapi is in lambdapi.bnf.
Identifiers
An identifier can be:
a regular identifier:
/
or an arbitrary non-empty sequence of UTF-8 codepoints not among\t\r\n :,;`(){}[]".@$|?/
an escaped identifier: an arbitrary sequence of characters enclosed between
{|
and|}
Remark: for any regular identifier i
, {|i|}
and i
are
identified.
Remark: Escaped identifiers or regular identifiers ending with a non-negative integer with leading zeros cannot be used for bound variable names.
Convention: identifiers starting with an uppercase letter denote
types (e.g. Nat
, List
), and identifiers starting with a
lowercase letter denote constructors, functions and proofs
(e.g. zero
, add
, refl
).
Qualified identifiers
A qualified identifier is an identifier of the form
dir1.
… dirn.file.id
denoting the function symbol id
defined
in the file dir1/
… /dirn/file.lp
. To be used, dir1.
…
dirn.file
must be required first.
Remark: dir1
, …, dirn
cannot be natural numbers.
Terms
A user-defined term can be either:
TYPE
, the sort for typesan unqualified identifier denoting a bound variable
a qualified or a non-qualified symbol previously declared in the current file or in some previously open module, possibly prefixed by
@
to disallow implicit argumentsan anonymous function
λ (x:A) y z,t
mappingx
,y
andz
(of typeA
forx
) tot
a dependent product
Π (x:A) y z,T
a non-dependent product
A → T
(syntactic sugar forΠ x:A,T
whenx
does not occur inT
)a
let f (x:A) y z : T ≔ t in u
constructionan application written by space-separated juxtaposition, except for symbols having an infix notation (e.g.
x + y
)an infix symbol application
x + y
an identifier wrapped in parentheses to access its notationless value (e.g.
(+)
)a metavariable application
?0.[x;y]
that has been generated previously.?0
alone can be used as a short-hand for?0.[]
.a pattern-variable application
$P.[x;y]
(in rules only).$P
alone can be used as a shorthand for$P.[]
, except under binders (to avoid mistakes)._
for an unknown term or a term we don’t care about. It will be replaced by a fresh metavariable in terms, or a fresh pattern variable in a rule left-hand side, applied to all the variables of the context.an integer between 0 and 2^30-1 if the builtins
"0"
and"+1"
are defineda term enclosed between square brackets
[
…]
for explicitly giving the value of an argument declared as implicit
Subterms can be parenthesized to avoid ambiguities.