Lean4
/-- Given `α : Sort u`, `nonemp : Nonempty α`, `p : α → Prop`, a context of free variables
`ctx`, and a pair of an element `val : α` and `spec : p val`,
`mk_sometimes u α nonemp p ctx (val, spec)` produces another pair `val', spec'`
such that `val'` does not have any free variables from elements of `ctx` whose types are
propositions. This is done by applying `Function.sometimes` to abstract over all the propositional
arguments. -/
def mk_sometimes (u : Level) (α nonemp p : Expr) : List Expr → Expr × Expr → MetaM (Expr × Expr)
| [], (val, spec) => pure (val, spec)
| (e :: ctx), (val, spec) => do
let (val, spec) ← mk_sometimes u α nonemp p ctx (val, spec)
let t ← inferType e
let b ← isProp t
if b then
do
let val' ← mkLambdaFVars #[e] val
pure
(mkApp4 (Expr.const ``Function.sometimes [Level.zero, u]) t α nonemp val',
mkApp7 (Expr.const ``Function.sometimes_spec [u]) t α nonemp p val' e spec)
else
pure (val, spec)
