Is it possible to do (Vector n).mk?

Stream: lean4

[Alok Singh]

I have this:

structure Vector (n : Nat) (Scalar := S) where
  data : Array Scalar
  pf : data.size = n := sorry
  deriving Repr, BEq
def testVector : Vector 2 := {data := #[1.0, 2.0]}

Is there a way to do something like (Vector 2).mk #[1,2]?

[Kim Morrison]

structure Vector (n : Nat) (Scalar := Nat) : Type where
  data : Array Scalar
  pf : data.size = n := by sorry
deriving Repr, BEq

def testVector : Vector 2 := Vector.mk #[3, 7]

[Eric Wieser]

Or even just `def testVector : Vector 2 := .mk #[3, 7] without the repeated Vector

[Alok Singh]

Is there a way that doesn't rely on something inferring the 2 from type
constraints like those examples?

[Siddhartha Gadgil]

May be worse than the above, but one way of not specifying 2 is

def testVector' := @Vector.mk _ _ #[3, 7] rfl

[Eric Wieser]

Does (.mk #[3, 7] : Vector 2) meet your requirement?

[Henrik Böving]

Vector.mk should take n as an implicit argument that you can just explicitly specific with (n := foo) no?

[Bolton Bailey]

docs#Vector.mk

[Bolton Bailey]

Hmm, bit disappointing that we get a 404 link for that

[Henrik Böving]

Why, does that function exist? I don't see it

[Adam Topaz]

Vector.mk = Subtype.mk

[Henrik Böving]

Right, but this function does not exist under this name. if you #check Vector.mk with vector imported you will not get it.

[Bolton Bailey]

I mean it exists in the code that Kim provided above

[Bolton Bailey]

Screenshot-2024-05-09-at-5.44.29PM.png

[Bolton Bailey]

I am able to mouseover it in the lean web editor, so why can't we have a docs entry for it?

[Henrik Böving]

Yeah because Vector up there is a customly defined structure and not an alias for Subtype like the real vector, what's your point with respect to the docs?

[Henrik Böving]

image.png

this is the "real" vector, it's a def, not a structure

[Bolton Bailey]

Ah, I see, I did not realize that this definition was different.

[Bolton Bailey]

Frankly, I somehow didn't make the connection that there was a definition five lines above that has the same name as a Mathlib definition, I guess its only possible because mathlib isn't imported.