Plausible inside functions

Stream: general

[GasStationManager]

I am trying to do property-based testing inside of executable functions. (See my recent blog post and related zulip thread for discussion of the motivation).

In particular, I would like to call plausible on a proof goal inside a function.
However, plausible often struggle to run. Example where plausible is confused inside a recursive function:

def f (x:Int) :{y:Int //y>x ∧ y≠ 0}
:=
if hcomp: x>=0 then
  ⟨ x+1, (by omega)⟩
else
  ⟨ f 0, by plausible⟩ --error: (kernel) declaration has free variables '_tmp✝'
termination_by (-x).toNat
decreasing_by{
  simp_wf
  omega
}

In this example, I know the tests can be executed; is
it possible to "force-exeute" the tests? Outside the function I can do something like #eval! Testable.check ..., But here I really want to test the subgoal inside the function. I.e. I want the
equivalent of the following manual check:

import Plausible
open Plausible

def f (x:Int) : IO {y:Int //y>x ∧ y≠ 0}
:=do
if hcomp: x>=0 then
  return ⟨ x+1, (by omega)⟩
else
  let res ← f 0
  let checkRes:Bool := res.val > x ∧ res.val ≠ 0
  if !checkRes then
    IO.println "failed check: res.val > x ∧ res.val ≠ 0"
  return ⟨res, by sorry⟩
termination_by (-x).toNat
decreasing_by{
  simp_wf
  omega
}

#eval! f 1
#eval! f 0
--etc

Can this behavior be implemented as a modified version of the plausible command? I am happy to try to work on this; would appreciate pointers on how best to start...