From 0d39f21ead5b15ed4267c92642c955a0dc68c3a3 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Mon, 23 Oct 2023 20:03:40 -0400 Subject: [PATCH] fix: monads --- Std/Tactic/TryThis.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Std/Tactic/TryThis.lean b/Std/Tactic/TryThis.lean index aacfdd50d9..88b6541a53 100644 --- a/Std/Tactic/TryThis.lean +++ b/Std/Tactic/TryThis.lean @@ -354,7 +354,7 @@ The parameters are: * `header`: a string that begins the display. By default, it is `"Try this: "`. -/ def addSuggestion (ref : Syntax) (s : Suggestion) (origSpan? : Option Syntax := none) - (header : String := "Try this: ") : CoreM Unit := do + (header : String := "Try this: ") : MetaM Unit := do logInfoAt ref m!"{header}{s}" addSuggestionCore ref #[s] header (isInline := true) origSpan? @@ -385,7 +385,7 @@ The parameters are: -/ def addSuggestions (ref : Syntax) (suggestions : Array Suggestion) (origSpan? : Option Syntax := none) (header : String := "Try these:") - (style? : Option SuggestionStyle := none) : CoreM Unit := do + (style? : Option SuggestionStyle := none) : MetaM Unit := do if suggestions.isEmpty then throwErrorAt ref "no suggestions available" let msgs := suggestions.map toMessageData let msgs := msgs.foldl (init := MessageData.nil) (fun msg m => msg ++ m!"\n• " ++ m)