MPCTT

Directory of Rocq Files

• Getting Started gs.v
• Basic Computational Type Theory bctt.v
• Propositions as Types pat.v
• Leibniz Equality leibniz.v
• Inductive Eliminators elim.v
• Existential Quantification exquant.v
• Arithmetic Pairing pairing.v
• Abstract Syntax syntax.v
• Certifying Functions and Sum Types certsum.v
• Certifying Functions and Sigma Types certsig.v
• Linear Arithmetic la.v
• More Types more.v
• Indexed Inductives indind.v
• Extensionality ext.v
• Excluded Middle and Double Negation xm.v
• Provability provability.v
• Least Witness Operators lwo.v
• Arithmetic Recursion arec.v
• Euclidean Division ediv.v
• Lists list.v
• EWOs ewo.v
• Finite Types finty.v
• Countable Types cty.v
• Propositional Deduction pds.v, solver.v
• Boolean Satisfiability bsat.v
• Regular Expression Matching regexp.v
• Abstract Reduction Systems ars.v
• Axiom CT and Semidecidability undec.v
• Inductive Equality indeq.v
• Well-Founded Recursion wfrec.v
• Aczel Trees and Hierarchy Theorems aczel.v
• List of tactics used
• List of commands used

Some chapters have teaser files that may be used for demos in lectures. For instance, teaser-gs.v and demo-gs.v for “Getting Started”.