Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Witeness bei predicate subtypes
Gibt es wie bei Sigma Types eine Möglichkeit einen Witness zu bekommen ? Also z.B. für < Nat | [x] P x > :
[x : < Nat | [x] P x >] getElem x (getElem soll die Funktion sein , die in diesem Falle einen Nat zurück gibt).
Das macht in dem Fall keinen sinn - < Nat | P x > ist ein subtype von Nat. Wenn ich bereits ein n : < Nat | P x > habe, hab ich also auch automatisch n : Nat 