Autosubst.Autosubst_Basics

Autosubst.Autosubst_Tactics

Autosubst.Autosubst_Derive

Autosubst.Autosubst

Autosubst.Autosubst_MMap

Autosubst.Autosubst_Classes

Autosubst.Autosubst_MMapInstances

Autosubst.Autosubst_Lemmas

Plain.Decidable

• Notation for decidable propositions

Plain.Demo

• Autosubst Tutorial
  • Syntax and the substitution operation
  • Reduction and substitutivity
  • Type Preservation

Plain.Context

• Context

Plain.Size

• Support for Size Induction

Plain.POPLmark

• POPLmark Part 1

Ssr.Context

• Context

Ssr.BetaSubstitution

• Correctness of Single Variable Substitutions

Ssr.pred_CC_omega

• Predicative CC omega: Type Preservation and Confluence

Ssr.AutosubstSsr

• Autosubst wrapper for ssreflect

Ssr.SystemF_SN

• Strong Normalization of System F

Ssr.SystemF_CBV

• Normalization of Call-By-Value System F

Ssr.ARS

• Abstract Reduction Systems

Ssr.POPLmark

• POPLmark Part 1a + 2a

Ssr.CR