From 45075c135d830548809010e61dc36d77696cf048 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Dec 2019 19:47:44 -0800 Subject: [PATCH] chore: move `ParserKind` to `LeanExt` --- src/Init/Lean/Parser/Parser.lean | 7 ++----- src/Init/LeanExt.lean | 5 ++++- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean index 00115a7f09..24432e1c80 100644 --- a/src/Init/Lean/Parser/Parser.lean +++ b/src/Init/Lean/Parser/Parser.lean @@ -192,15 +192,12 @@ match s with end ParserState -inductive ParserKind -| leading | trailing - -export ParserKind (leading trailing) - def ParserArg : ParserKind → Type | ParserKind.leading => Nat | ParserKind.trailing => Syntax +export ParserKind (leading trailing) + def BasicParserFn := ParserContext → ParserState → ParserState def ParserFn (k : ParserKind) := ParserArg k → BasicParserFn diff --git a/src/Init/LeanExt.lean b/src/Init/LeanExt.lean index edc3d3bcef..15e118d72e 100644 --- a/src/Init/LeanExt.lean +++ b/src/Init/LeanExt.lean @@ -23,10 +23,13 @@ inductive Name | str : Name → String → USize → Name | num : Name → Nat → USize → Name +inductive ParserKind +| leading | trailing + /- Small DSL for describing parsers. We implement an interpreter for it at `Parser.lean` -/ -inductive ParserDescr +inductive ParserDescr (kind : ParserKind := ParserKind.leading) | andthen : ParserDescr → ParserDescr → ParserDescr | orelse : ParserDescr → ParserDescr → ParserDescr | optional : ParserDescr → ParserDescr