Data.SBV.Examples.Uninterpreted.Deduce

Representing uninterpreted booleans

data B

type SB

Uninterpreted connectives over B

and

or

not

Axioms of the logical system

ax1

ax2

ax3

Demonstrated deduction

test