The Pie à-let-mode Reference
1 Pie à-let-mode Specific Expressions

The Pie à-let-mode Reference

Andrew M. Kent

Pie à-let-mode is a tasty little fork of Pie–the little language with dependent types that accompanies The Little Typer–which adds the let and equal 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

1 Pie à-let-mode Specific Expressions

local bindings

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

equational rewriting

(equal type term clause ...+)

clause = #:by proof term
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 ...))