diff options
Diffstat (limited to 'proofs/signatures/lrat.plf')
| -rw-r--r-- | proofs/signatures/lrat.plf | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/proofs/signatures/lrat.plf b/proofs/signatures/lrat.plf index ae6cbd101..ea1d90537 100644 --- a/proofs/signatures/lrat.plf +++ b/proofs/signatures/lrat.plf @@ -18,6 +18,14 @@ (program bool_or ((l bool) (r bool)) bool (match l (ff r) (tt tt))) (program bool_and ((l bool) (r bool)) bool (match l (tt r) (ff ff))) (program bool_not ((b bool)) bool (match b (tt ff) (ff tt))) +(program bool_eq ((l bool) (r bool)) bool + (match l + (tt (match r + (tt tt) + (ff ff))) + (ff (match r + (tt ff) + (ff tt))))) ; =================== ; ; Working CNF formula ; |