Lean4
/-- Log error message that will displayed to the user at the end.
Messages are logged only when `transitionDepth = 0` i.e. when `fun_prop` is **not** trying to infer
function property like continuity from another property like differentiability.
The main reason is that if the user forgets to add a continuity theorem for function `foo` then
`fun_prop` should report that there is a continuity theorem for `foo` missing. If we would log
messages `transitionDepth > 0` then user will see messages saying that there is a missing theorem
for differentiability, smoothness, ... for `foo`. -/
def logError (msg : String) : FunPropM Unit := do
if (← read).transitionDepth = 0 then
modify fun s => { s with msgLog := if s.msgLog.contains msg then s.msgLog else msg :: s.msgLog }
