Project Page Index Table of Contents

Library DProp.Prop

  • Syntax
  • Model theory
  • Proof theory
  • Relating proofs to truths
  • Commentary
    • Understanding Incompleteness
    • Why is incompleteness important? Or is it?
    • Does this mean natural numbers can't be defined?
    • Interpreting into Prop and bool

Library DProp.Tactics

Library DProp.Prop_solutions

  • Syntax
  • Model theory
  • Proof theory
  • Relating proofs to truths
  • Commentary
    • Understanding Incompleteness
    • Why is incompleteness important? Or is it?
    • Does this mean natural numbers can't be defined?
    • Interpreting into Prop and bool
Generated by coqdoc and improved with CoqdocJS