Examples
-
Balanced Parentheses as an Embedded LanguageLet's look at how to use macros to extend the Lean 4 parser and embed a language for building balanced parentheses. This language accepts strings given by the BNF grammarDyck ::= "(" Dyck ")" |...Read more
-
Arithmetic as an Embedded LanguageLet's parse another classic grammar, the grammar of arithmetic expressions with addition, multiplication, integers, and variables. In the process, we'll learn how to:Convert identifiers such as x...Read more
-
PalindromesPalindromes are lists that read the same from left to right and from right to left. For example, [a, b, b, a] and [a, h, a] are palindromes.We use an inductive predicate to specify whether a list is a...Read more
-
Binary Search TreesIf the type of keys can be totally ordered -- that is, it supports a well-behaved ≤ comparison -- then maps can be implemented with binary search trees (BSTs). Insert and lookup operations on BSTs...Read more
-
A Certified Type CheckerIn this example, we build a certified type checker for a simple expression language.Remark: this example is based on an example in the book Certified Programming with Dependent Types by Adam...Read more
-
Dependent de Bruijn IndicesIn this example, we represent program syntax terms in a type family parameterized by a list of types, representing the typing context, or information on which free variables are in scope and...Read more
-
Parametric Higher-Order Abstract SyntaxIn contrast to first-order encodings, higher-order encodings avoid explicit modeling of variable identity. Instead, the binding constructs of an object language (the language being formalized) can be...Read more