## Stream: general

### Topic: quotient.lift_on elaboration

#### Kenny Lau (Jul 06 2019 at 04:23):

import data.set.basic

-- works
example {α β : Type*} [setoid α] (s : set β) [setoid s]
(f : α → β) (hf1 : ∀ x, f x ∈ s) (hf2 : ∀ x y, x ≈ y → (⟨f x, hf1 x⟩ : s) ≈ ⟨f y, hf1 y⟩) :
quotient _inst_1 → quotient _inst_2 :=
λ x, quotient.lift_on x (λ r, ⟦(⟨f r, hf1 r⟩ : s)⟧) $λ x y hxy, quotient.sound$ hf2 x y hxy

/-
invalid constructor ⟨...⟩, expected type is not an inductive type
?m_1
-/
example {α β : Type*} [setoid α] (s : set β) [setoid s]
(f : α → β) (hf1 : ∀ x, f x ∈ s) (hf2 : ∀ x y, x ≈ y → (⟨f x, hf1 x⟩ : s) ≈ ⟨f y, hf1 y⟩) :
quotient _inst_1 → quotient _inst_2 :=
λ x, quotient.lift_on x (λ r, ⟦⟨f r, hf1 r⟩⟧) $λ x y hxy, quotient.sound$ hf2 x y hxy


#### Kenny Lau (Jul 06 2019 at 04:24):

why does it fail when I have an inductive type?

#### Mario Carneiro (Jul 06 2019 at 04:54):

it's an elaboration order problem. Anonymous constructors must resolve to an inductive type straight away, but I guess the other stuff is getting elaborated before lean knows what the target type is of the function

Last updated: May 18 2021 at 16:25 UTC