pub fn native_decide(ctx: &Context, prop: &Term, inst: &Term) -> Option<Term>Expand description
Build a native_decide proof of prop from a Decidable prop instance inst: if the
decision procedure NATIVELY evaluates to true, return the proof term
of_decide_eq_true prop inst (ofReduceBool (decide prop inst) true (refl Bool true)),
which the (main) kernel checks by running this evaluator via the reduceBool hook —
never by re-normalizing the decision procedure. Returns None (fail-safe) when the
decision is not true, so it can only ever produce proofs of genuinely-true goals.