• Home
• About Coq
• Get Coq
• Documentation
• Community

Library lc.Slc

• Syntactic Lambda calculus
  • Notations
  • Inductive datatype of terms

Library lc.Quot

• Equivalence relations and quotients
  • Equivalence relations
  • Quotients

Library lc.Monad

• Monads
  • Notations
  • Definition of monad.
  • Monad morphisms

Library lc.Mod

• Modules
  • Notations
  • Definition of module of a monad.
  • Tautological module
  • Pull-back module

Library lc.Misc

• Miscellanea
  • Handy terms for option
  • An useful hint.

Library lc.Lc

• Simple (untyped) Lambda Calculus

Library lc.Extensionality

• Axiom of extensionality

Library lc.Derived_Mod

• Derived Module
• Exponetial Monads

• webmaster
• xhtml valid
• CSS valid