• Skip to primary navigation
  • Skip to content
  • Skip to footer
Arend Theorem Prover
  • About
  • Documentation
  • Download
    • Getting Started
    • Language Reference
      • Lexical structure
      • Definitions
      • Expressions
      • Prelude
    • Tutorial
      • Part I: Dependent Types
      • Part II: Homotopy Type Theory
    • Libraries
    • Standard metas
      • Unclassified metas
      • Paths metas
      • Functional metas
      • Algebraic metas
      • Logical metas
      • Debugging metas

    Language Reference

    This section contains the specification of the Arend language.

    • Lexical structure
    • Definitions
      • Modules
      • Parameters
      • Functions
      • Type synonyms
      • Data
      • Higher inductive types
      • Records
      • Classes
      • Meta definitions
      • Coercion
      • Level
    • Expressions
      • Goals
      • Universes
      • Pi types
      • Sigma types
      • Let
      • Case
      • Class extensions
      • Box
    • Prelude
    • GitHub
    • Twitter
    • Feed
    © 2023 Arend. Powered by Jekyll & Minimal Mistakes.