Zulip Chat Archive

Stream: new members

Topic: Little typeclass thing


view this post on Zulip Kevin Sullivan (Mar 07 2021 at 17:42):

I notice that the following code works but the following simple replacement breaks it.

Change this code at the end

 let mop := m.op in (mop _ _)

to this seemingly equivalent code

(m.op _ _)

What am I missing here?

import algebra

-- test import
#check has_mul
#check semigroup
#check has_one
#check monoid

namespace alg

universe u

/-
Stack of three typeclasses, each extending from the previous
-/

@[class]
structure my_has_one (α : Type u) :=
(one : α)

/-
has_op
-/

@[class]
structure has_op (α : Type u) :=
(op : α  α  α)


/-
ext_has_op extends from has_op
-/
@[class]
structure ext_has_op (α : Type u) extends has_op α :=
(b : bool)


/-
ext_ext_has_op: optiplicative semigroup plus optiplicative one
-/
@[class]
structure ext_ext_has_op (α : Type u) extends ext_has_op α :=
(s : string)



/-
Instances for nat
-/

@[instance]
def has_one_nat : my_has_one nat :=  1 

/-
haz_op nat instance
-/
@[instance]
def has_op_nat : has_op nat :=  nat.mul 


/-
ext_has_op nat instance
-/
instance ext_has_op_nat : ext_has_op nat :=  tt 

/-
ext_ext_has_op nat instance
-/
instance ext_ext_has_op_nat : ext_ext_has_op nat :=  "Hello" 

/-
set_option trace.class_instances true
set_option class.instance_max_depth 20
-/

def mul_foldr
  {α : Type u}
  [m : ext_ext_has_op α]
  [o : my_has_one α]
  :
  list α  α
| [] := o.one
| (h::t) :=
let mop := m.op in
    mop h (mul_foldr t)                     -- Change code here

#eval mul_foldr [1,2,3,4,5]

end alg

Last updated: May 13 2021 at 06:15 UTC