26 lines
837 B
Text
26 lines
837 B
Text
structure_instance_bug3.lean:1:23: error: invalid structure value { ... }, field 'pure_bind' was not provided
|
||
structure_instance_bug3.lean:1:23: error: invalid structure value { ... }, field 'bind_assoc' was not provided
|
||
structure_instance_bug3.lean:1:23: error: failed to synthesize type class instance for
|
||
⊢ has_pure set
|
||
structure_instance_bug3.lean:1:23: error: failed to synthesize type class instance for
|
||
⊢ has_bind set
|
||
structure_instance_bug3.lean:1:23: error: exact tactic failed, type mismatch, given expression has type
|
||
?m_2 = ?m_2
|
||
but is expected to have type
|
||
x >>= has_pure.pure set ∘ f = set.image f x
|
||
state:
|
||
3 goals
|
||
α β : Type ?,
|
||
f : α → β,
|
||
x : set α
|
||
⊢ x >>= has_pure.pure set ∘ f = set.image f x
|
||
|
||
α β : Type ?,
|
||
f : α → β,
|
||
x : set α
|
||
⊢ Sort ?
|
||
|
||
α β : Type ?,
|
||
f : α → β,
|
||
x : set α
|
||
⊢ ?m_1
|