Welcome to Mikan’s documentation!

This is the manual for the Mikan programming language, its type checking, compilation and editing system and related resources/tools.

Warning

This user manual is in the process of being updated and may contain outdated or inaccurate information.

• Language Reference
  • Abstract definitions
  • Built-ins
  • Coinduction
  • Copatterns
  • Core language
  • Coverage Checking
  • Cubical
  • Cubical compatible
  • Cumulativity
  • Data Types
  • Function Definitions
  • Function Types
  • Generalization of Declared Variables
  • Implicit Arguments
  • Instance Arguments
  • Lambda Abstraction
  • Local Definitions: let and where
  • Lexical Structure
  • Literal Overloading
  • Lossy Unification
  • Mixfix Operators
  • Module System
  • Mutual Recursion
  • Opaque definitions
  • Pattern Synonyms
  • Positivity Checking
  • Postulates
  • Pragmas
  • Prop
  • Record Types
  • Reflection
  • Safe Agda
  • Sort System
  • Syntactic Sugar
  • Syntax Declarations
  • Telescopes
  • Termination Checking
  • Two-Level Type Theory
  • Universe Levels
  • With-Abstraction
  • Without K
• Tools
  • Automatic Proof Search (Auto)
  • Command-line options
  • Debugging
  • Emacs Mode
  • Literate Programming
  • Generating HTML
  • Generating LaTeX
  • Interface files
  • Library Management
  • Performance debugging
  • Search Definitions in Scope
• Contribute
  • Documentation
• The Mikan Team and License

• Index