Documentation

Lean.Parser.Do

@[inline]
Instances For

    A doSeq is a sequence of doElem, the main argument after the do keyword and other do elements that take blocks. It can either have the form "{" (doElem ";"?)* "}" or many1Indent (doElem ";"?), where many1Indent ensures that all the items are at the same or higher indentation level as the first line.

    Instances For

      termBeforeDo is defined as withForbidden("do", term), which will parse a term but disallows do outside of a bracketing construct. This is used for parsers like for _ in t do ... or unless t do ..., where we do not want t do ... to be parsed as an application of t to a do block, which would otherwise be allowed.

      Instances For

        for x in e do s iterates over e assuming e's type has an instance of the ForIn typeclass. break and continue are supported inside for loops. for x in e, x2 in e2, ... do s iterates of the given collections in parallel, until at least one of them is exhausted. The types of e2 etc. must implement the ToStream typeclass.

        Instances For

          break exits the surrounding for loop.

          Instances For

            continue skips to the next iteration of the surrounding for loop.

            Instances For

              return e inside of a do block makes the surrounding block evaluate to pure e, skipping any further statements. Note that uses of the do keyword in other syntax like in for _ in _ do do not constitute a surrounding block in this sense; in supported editors, the corresponding do keyword of the surrounding block is highlighted when hovering over return.

              return not followed by a term starting on the same line is equivalent to return ().

              Instances For

                unless e do s is a nicer way to write if !e do s.

                Instances For

                  return used outside of do blocks creates an implicit block around it and thus is equivalent to pure e, but helps with avoiding parentheses.

                  Instances For