Then why are we all so interested?

Examples provide more than syntax. It's the semantics that we care about most.

▲ aleph_minus_one 4 hours ago | parent [-]

> Examples provide more than syntax. It's the semantics that we care about most.

... and this semantics is explained in a quite encompassing way in the introductory notes "Proof-Oriented Programming in F*":

> https://fstar-lang.org/tutorial/proof-oriented-programming-i...

> https://fstar-lang.org/tutorial/

▲ derdi 8 minutes ago | parent [-]

The OP doesn't want encompassing, they want the following example from the tutorial on the front page:

    type vec (a:Type) : nat -> Type =
      | Nil : vec a 0
      | Cons : #n:nat -> hd:a -> tl:vec a n -> vec a (n + 1)
    
    let rec append #a #n #m (v1:vec a n) (v2:vec a m)
      : vec a (n + m)
      = match v1 with
        | Nil -> v2
        | Cons hd tl -> Cons hd (append tl v2)

This is a completely reasonable thing to want and expect.