casting from Prop/bool to semiring

Stream: general

[Kenny Lau]

Do we have a function that sends a prop/bool to 1 if it is true and 0 if it is false?

[Keeley Hoek]

There is no instance for semiring bool in mathlib I think

[Neil Strickland]

import algebra.ring

instance : discrete_field bool :=
begin
 refine_struct {
  zero := ff, one := tt,
  neg := id, inv := id,
  add := bxor, mul := band,
  zero_ne_one := λ e, by {cases e},
  has_decidable_eq := by { apply_instance }
 };
 try { repeat { intro a, cases a }; exact dec_trivial, },
end