DCOIOmega.Autosubst2.axioms

• General Header Autosubst - Assumptions and Definitions
  • Axiomatic Assumptions
  • Functor Instances

DCOIOmega.Autosubst2.syntax

DCOIOmega.Autosubst2.unscoped

• Autosubst Header for Unnamed Syntax
  • Primitives of the Sigma Calculus.
  • Type Class Instances for Notation
  • Proofs for the substitution primitives.
  • Notations for unscoped syntax
  • Tactics for unscoped syntax

DCOIOmega.Lattice.All

• Signature for lattices
  • An incomplete solver for lattice formulas

DCOIOmega.admissible

DCOIOmega.consistency

DCOIOmega.conv

DCOIOmega.factorization

DCOIOmega.geq

DCOIOmega.iconv_dec

DCOIOmega.imports

DCOIOmega.normalform

DCOIOmega.par

DCOIOmega.preservation

DCOIOmega.semtyping

DCOIOmega.soundness

DCOIOmega.toplevel

DCOIOmega.typing

DCOIOmega.typing_conv