map out of restricted comprehension

Stream: lean4

[Dean Young]

How would you construct a map out of a restricted comprehension?

variable {X : Type 1}
variable {B : Type 1}
variable {p : X -> Prop}
def A := {x : X // p x }
def f : A -> B := ???

[Kevin Buzzard]

variable {X : Type 1}
variable {B : Type 1}
variable (p : X -> Prop)
def A := {x : X // p x }
def f : A p -> B := λ ⟨x, hx⟩ => _
def f' : A p -> X := λ a => a.val
def f'' : A p -> A p := λ a => ⟨a.val, a.property⟩

[Dean Young]

Kevin Buzzard said:

variable {X : Type 1}
variable {B : Type 1}
variable (p : X -> Prop)
def A := {x : X // p x }
def f : A p -> B := λ ⟨x, hx⟩ => _
def f' : A p -> X := λ a => a.val
def f'' : A p -> A p := λ a => ⟨a.val, a.property⟩

I get

Main.lean:54:28: error: invalid pattern, constructor or constant marked with '[match_pattern]' expected

[Kevin Buzzard]

Are you on an up to date version of lean 4?

[Dean Young]

Kevin Buzzard said:

Are you on an up to date version of lean 4?

I managed to fix it thanks :)