From dc5652210cd60b229d0bbe9900b9d68ebbda5dfd Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Mon, 16 Aug 2021 16:22:16 +0200 Subject: [PATCH] fix: missing instance --- src/Lean/Widget/TaggedText.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Lean/Widget/TaggedText.lean b/src/Lean/Widget/TaggedText.lean index 68c6b2a2dd..7b1992c1d3 100644 --- a/src/Lean/Widget/TaggedText.lean +++ b/src/Lean/Widget/TaggedText.lean @@ -44,8 +44,8 @@ partial def map : TaggedText α → TaggedText β | append as => append (as.map map) | tag t a => tag (f t) (map a) -variable (f : α → m β) in -partial def mapM [Monad m] : TaggedText α → m (TaggedText β) +variable [Monad m] (f : α → m β) in +partial def mapM : TaggedText α → m (TaggedText β) | text s => text s | append as => do append (← as.mapM mapM) | tag t a => do tag (← f t) (← mapM a) @@ -56,9 +56,9 @@ partial def rewrite : TaggedText α → TaggedText β | append as => append (as.map rewrite) | tag t a => f t a -variable (f : α → TaggedText α → m (TaggedText β)) in +variable [Monad m] (f : α → TaggedText α → m (TaggedText β)) in /-- Like `mapM` but allows rewriting the whole subtree at `tag` nodes. -/ -partial def rewriteM [Monad m] : TaggedText α → m (TaggedText β) +partial def rewriteM : TaggedText α → m (TaggedText β) | text s => text s | append as => do append (← as.mapM rewriteM) | tag t a => f t a