Proof checking experiments folder

FormalSAT / trestle

Apache License 2.0

18 stars 2 forks source link

Proof checking experiments folder #16

Closed ccodel closed 8 months ago

ccodel commented 8 months ago

Lots of basic lemmas on Arrays, and some new reasoning in PropFun about lattices, complements, and eqsat.

JamesGallicchio commented 8 months ago

addresses #13

JamesGallicchio commented 8 months ago

I'm trying to keep the core sorry-free. Are you using the sorry'd lemmas in PPA? maybe we put the setF file in experiments with the PPA implementation