Feature request: dependent type , proof assistant

[zaoqi]

https://docs.racket-lang.org/pie/index.html
https://docs.racket-lang.org/ts-reference/Experimental_Features.html#%28part._.Dependent_.Function_.Types%29
https://www.idris-lang.org/
https://en.wikipedia.org/wiki/Agda_(programming_language)
https://en.wikipedia.org/wiki/Dependent_type
https://en.wikipedia.org/wiki/Proof_assistant

[ntrel]

I looked at the intro for the Wikipedia link for DT. I think as V has optional types and private struct fields, we can enforce that a field is never constructed with a value it should not hold. The constructor function for a struct OddInt would be:

struct OddInt {
  i int
}
fn odd_int(i int) OddInt? {
  return if i & 1 {OddInt{i}} else {none}
}

Edit: fix struct.

[zaoqi]

@ntrel
[WARNING]The following text was generated by Google Translate
This probably has little to do with DT.
You can read "The Little Typer" to learn about DT.

[zaoqi]

Anything you can do in other languages, you can do in V. ?

I can not do something I can do in Idris,Agda,... in V.