From 3f883bd9499e6f0641c5b699aa113e7ec49c41bb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 9 May 2018 09:19:14 -0700 Subject: [PATCH] chore(library/init/lean/parser/parser): add `monad_fail` instance --- library/init/lean/parser/parser.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean index 5d9b83e9c4..54c8f4dc58 100644 --- a/library/init/lean/parser/parser.lean +++ b/library/init/lean/parser/parser.lean @@ -9,7 +9,7 @@ https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/parsec-paper -/ prelude import init.data.to_string init.data.string.basic init.data.list.basic init.control.except -import init.data.repr init.lean.name init.data.dlist +import init.data.repr init.lean.name init.data.dlist init.control.monad_fail namespace lean namespace parser @[reducible] def position : Type := nat @@ -104,6 +104,9 @@ protected def bind (p : parser α) (q : α → parser β) : parser β := instance : monad parser := { bind := @parser.bind, pure := @parser.pure } +instance : monad_fail parser := +{ fail := λ _ s it, error { unexpected := s, pos := it.offset } ff } + def expect (msg : message) (exp : string) : message := {expected := dlist.singleton exp, ..msg}