fact: Definition fullAdder carry b1 b2 : bool * bool := match carry, b1, b2 with | false, false, false => (false, false) | true, false, false | false, true, false | false, false, true => (false, true) | true, true, false | false, true, true | true, false, true => (true, false) | true, true, true => (true, true) end.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq tuple) spec