The two internal representations, LightfoldAST and LightfoldCore, are defined as abstract data types using signatures with Σ-terms and fold functions as introduced in [section @sec:theory:algebraic]. Parsing is done directly into an LightfoldAST-algebra as explained in [section @sec:methods:algebraic]. Using an algebra targeting LightfoldCore, we get a LightfoldCore program.

LightfoldCore as the main internal representation of Lightfold programs is closely based on the dependently typed lambda calculus \lp introduced with its rules for evaluation and typing in [section @sec:dependent]. We use a core language close to the base calculus to allow for easi application of the various theoretical methods from [chapter @sec:theory].

LightfoldCore as the main internal representation of Lightfold programs is closely based on the dependently typed lambda calculus \lp introduced with its rules for evaluation and typing in [section @sec:dependent]. We use a core language close to the base calculus to allow for easier application of the various theoretical methods from [chapter @sec:theory].

Type checking and evaluation is performed on LightfoldCore terms using recursive algorithms based on the typing and evaluation rules. That shows another advantage of using a small core language: It keeps Lightfold extensible. Features can be added without changes to the core part of the language, as long as they can be translated into LightfoldCore.

...

...

@@ -170,7 +170,7 @@ Nat : Type

succ Nat

```

Note that while identifiers are case-sensitive, Lightfold does not impose any restrictions as to the case of the identifiers used in definitions, binders and variables. However, we generally use upper-case identifiers for types and lower-case identifiers in all other occasions.

Note that while identifiers are case-sensitive, Lightfold does not impose any restrictions on the case of the identifiers used in definitions, binders and variables. However, we generally use upper-case identifiers for types and lower-case identifiers in all other occasions.

The resulting formal syntax rules are shown in [definition @fig:def:syntax].