Zulip Chat Archive

Stream: general

Topic: casting from Prop/bool to semiring


Kenny Lau (May 27 2019 at 12:20):

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

Keeley Hoek (May 27 2019 at 12:24):

There is no instance for semiring bool in mathlib I think

Neil Strickland (May 27 2019 at 12:29):

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

Last updated: Dec 20 2023 at 11:08 UTC