Zulip Chat Archive

Stream: general

Topic: simp changes with_top to with_bot

view this post on Zulip Gabriel Ebner (Oct 30 2019 at 15:52):

I was somewhat to surprised that with_bot.coe_add can not only rewrite with_top, but the result then contains typeclass instances for with_bot... (This caused apply and rw to fail later on, but I'm not exactly sure why.)

import algebra.ordered_group

set_option pp.implicit true
set_option pp.notation false
example (x y : nat) : ((x + y : nat) : with_top nat) = (42 : nat) :=
  trace_state, -- look at the has_add instance

Last updated: May 06 2021 at 22:13 UTC