Zulip Chat Archive

Stream: lean4

Topic: Subtypes


view this post on Zulip Xevi Roca (Mar 08 2021 at 11:05):

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] ?

view this post on Zulip Kenny Lau (Mar 08 2021 at 11:07):

#backticks

view this post on Zulip Xevi Roca (Mar 08 2021 at 11:09):

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] ?

view this post on Zulip Johan Commelin (Mar 08 2021 at 11:15):

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

view this post on Zulip Xevi Roca (Mar 08 2021 at 11:21):

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


Last updated: May 07 2021 at 13:21 UTC