Project Page Index Table of Contents
  • Preliminaries
    • Decidable propositions
    • Discrete types and decidable predicates
    • Pure predicates
    • Subtypes for normalizers on discrete types
  • HF Structures
  • Tactic hfs
  • Extensionality and Decidability
  • Categoricity
  • Operations
  • Transitive Closure
  • Binary Trees
  • Tree Model of HF
  • Ordinals
  • Cardinality
    • Cardinality relation
    • Cardinality function
  • Ackermann Model of HF
Generated by coqdoc and improved with CoqdocJS