From 9bd953d0405253d2e1d7eca7a1187aa4f3fbe130 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Thu, 18 Jun 2026 03:40:44 -0400 Subject: [PATCH] fix: universe issue --- Parser/Basic.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Parser/Basic.lean b/Parser/Basic.lean index 8073c041..ddee1c3f 100644 --- a/Parser/Basic.lean +++ b/Parser/Basic.lean @@ -192,13 +192,12 @@ returned values of `p`. Consumes no input on error. def takeManyN (n : Nat) (p : ParserT ε σ τ m α) : ParserT ε σ τ m (Array α) := withBacktracking do foldl Array.push (← take n p) p -set_option linter.checkUnivs false in /-- `takeUntil stop p` parses zero or more occurrences of `p` until `stop` succeeds, and returns the array of returned values of `p` and the output of `stop`. If `p` fails before `stop` is encountered, the error from `p` is reported and no input is consumed. -/ -partial def takeUntil (stop : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) : +partial def takeUntil {α β : Type u_1} (stop : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) : ParserT ε σ τ m (Array α × β) := have := Inhabited.mk do return ((#[] : Array α), (← stop)) withBacktracking do rest #[]