Type Theory

This section covers the type theory and axioms used by Lean.

  • cover CiC
  • axiom-k, fun-ext, strong indefinite description? this should be refined

results matching ""

    No results matching ""