Subtypes

Stream: lean4

[Xevi Roca]

If I use
abbrev Vector α n := { a : Array α // a.size = n }
how I should create a Vector Nat 3 from the Array
#[1,2,3] ?

[Kenny Lau]

#backticks

[Xevi Roca]

If I use
abbrev Vector α n := { a : Array α // a.size = n }
how I should create a Vector Nat 3 from the Array
#[1,2,3] ?

[Johan Commelin]

I've never used Lean 4, but probably ⟨[1,2,3], rfl⟩

[Xevi Roca]

Thanks ! It worked if put # before the list [1,2,3]

This is how a checked:

abbrev Vector α n := { a : Array α // a.size = n }

def v: Vector Nat 3 := ⟨#[1,2,3], rfl⟩
#check v
#eval v

Thanks again