Skip to content

Partial def

Viktor Kuncak requested to merge github/fork/SimonGuilloud/partialDef into main

Created by: SimonGuilloud

Ability to do sub-specified definitions. If you want an object with propriety P(x), you can feed a proof of unique existence of Q(x) as long as Q is OL-smaller than P (so in particular it holds if Q=P/\S). There is an example with a non-empty set in Exercise.scala.

Merge request reports