Project Page Index Table of Contents

Autosubst.Autosubst2
  • Autosubst 2
    • Canonical Structures for Substitutions
    • Asimpl
    • Recursive Simplification
    • Reflection Helpers (from Krebbers' std++ library)
    • Simplifying Index Expressions
    • Simplifying Renamings
    • Simplifying Substitutions
    • AsimplCons
    • AsimplVar

Autosubst.SystemF_cbv

Autosubst.axioms
    • Propositional extensionality
    • Functional extensionality
    • Extensionality for products
    • Extensionality Tactic
    • Typeclass instance for Funext

Autosubst.sem
  • Normalization of Call-By-Value System F
    • Notations
    • Call-by value reduction
    • Syntactic typing
    • Semantic typing
    • Applications
Generated by coqdoc and improved with CoqdocJS