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.
Then why are we all so interested?
Examples provide more than syntax. It's the semantics that we care about most.
> 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/
The OP doesn't want encompassing, they want the following example from the tutorial on the front page:
This is a completely reasonable thing to want and expect.
Edit: For comparison, Rocq https://rocq-prover.org/ and Lean https://lean-lang.org/ both manage to do this.
1 reply →