theorem abstain_builds_a_silent_rule : (abstain "him" on "/logs").outcome = .notApplicable := by⊢ { equivalent := fun req => req.user == "him" && req.resource == "/logs", outcome := Decision.notApplicable }.outcome = Decision.notApplicable auth_proveAll goals completed! 🐙 /-- "abstain him on /logs" → the policy stays silent about him. -/ theorem inline_abstain_is_silent : evaluate [abstain "him" on "/logs"] ⟨"him", "read", "/logs"⟩ = .notApplicable := by⊢ evaluate [{ equivalent := fun req => req.user == "him" && req.resource == "/logs", outcome := Decision.notApplicable }] { user := "him", action := "read", resource := "/logs" } = Decision.notApplicable auth_proveAll goals completed! 🐙