projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8b41e8d) | patch
Add working example of LFSC proof with quantifiers. Update quantifiers signature...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 13 Mar 2014 14:58:07 +0000 (09:58 -0500)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 13 Mar 2014 14:58:07 +0000 (09:58 -0500)
commit2b2c656543cc4ee7051ff00211a56f45331a763c
tree4e54f86ac7446d32b58282fca362851c716cc151tree
parent8b41e8d8128752eba75f32f751ec9c095a6b1d87commit | diff
Add working example of LFSC proof with quantifiers.  Update quantifiers signature to avoid dependent types in side condition.
proofs/signatures/example-quant.plf [new file with mode: 0755] blob
proofs/signatures/th_quant.plf diff | blob | history