メモ。#print opaque

To be fair, it's not too hard to find out whether a function depends on a partial function, you can use `#print opaques` for this purpose: ``` import Batteries.Tactic.PrintOpaques partial def ohNo (n : Nat) : Nat := ohNo n def badDefinition (a : Nat) : Nat := ohNo a + 2 /-- info: 'badDefinition' depends on opaque or partial definitions: [ohNo] -/ #guard_msgs in #print opaques badDefinition ``` And if you wanted, you could also add attributes and linters and whatnot for yourself that provide errors when you use a partial function