theory_datatype Directory Reference

Files

• file datatype_proof_rules.h [code]

  Abstract interface for recursive datatype proof rules.
  

• file datatype_theorem_producer.cpp [code]

  TRUSTED implementation of recursive datatype rules.
  

• file datatype_theorem_producer.h [code]

  TRUSTED implementation of recursive datatype proof rules.
  

• file theory_datatype.cpp [code]
• file theory_datatype2.cpp [code]
• file theory_datatype_lazy.cpp [code]

---