typecheck

Documentation

Overview

Example typecheck demonstrates basic type checking with the HoTT kernel.

This example shows how to:

• Parse terms from S-expression syntax
• Create a type checker with primitive types
• Synthesize types for terms
• Check terms against expected types
• Handle type errors