leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: help with rewriting simple tactic


Joe Palermo (Apr 21 2021 at 19:54):

How can I rewrite the following tactic in such a way that the return value is just 'bool' i.e. not 'tactic bool'?

meta def can_parse (parser : string -> tactic pexpr) (input : string) : tactic bool :=
  (parser input) >> return tt <|> return ff

Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll