The Pie à-let-mode Reference
Pie à-let-mode is a
little fork of
–the little language with dependent types that
accompanies The Little Typer
–which adds the let
forms. All other forms are identical to Pie;
consult the documentation for Pie for more information on
the rest of the language.
1 Pie à-let-mode Specific Expressions
(let ([id id-expr] ...) expr)
Binds id-expr to id for any proceeding bindings
and for the body expr. i.e. acts like Racket’s
let*. This form is checked in synthesis mode.
(equal type term clause ...+)
Allows for simple equational rewriting.
(equal X term1 #:by proof term2) is equivalent to
(the (= X term1 term2) proof).
(equal X term1 #:by proof term2 clause ...+)
is equivalent to (trans (the (= X term1 term2) proof)
(equal X term2 clause ...))