Sequence

Difficulty: moderate — 0 definitions, 0 abbreviations, 0 lemmas, 0 theorems, 0 examples.

definition theorem

legend

Sequences written the way they are written on paper: \(a_1, \dots, a_n\), freely mixing single entries with stretches standing for many at once. This module gives that reading a notation, so a statement about a distinguished position in a sequence can be written directly.

Logic uses it for the premises and conclusions of a rule, but nothing here is about logic: an entry is anything at all, and a stretch is a list of them.

ToSeq

What may stand as one entry in a sequence: a single item, or a whole list of them. This is what lets the notation below mix the two.

structure ToSeq (α β : Type) : Type

Read the entry as a list.
```
toSeq : β → List α
```

Show details

Outer dependencies: (none)

Lean core dependencies: Eq, HEq, List, eq_of_heq

Used by: instToSeq, instToSeqList

instToSeq

instance instToSeq {α : Type} : ToSeq α α

Show details

| instToSeq = { toSeq := fun a => [a] }

Complexity: 19 (size of the value term)

Outer dependencies: ToSeq

instToSeqList

instance instToSeqList {α : Type} : ToSeq α (List α)

Show details

| instToSeqList = { toSeq := fun P => P }

Complexity: 15 (size of the value term)

Outer dependencies: ToSeq

Lean core dependencies: List

toSeq_single

A single item contributes just itself.

theorem toSeq_single {α : Type} (a : α) : ⟪a⟫ = [a]

Show details

fun {α} a => rfl

Complexity: 21 (size of the value term)

Dependencies: instToSeq

Lean core dependencies: Eq, List, rfl

Used by: (none)

toSeq_list

A list contributes all of its items, spliced in.

theorem toSeq_list {α : Type} (P : List α) : ⟪P⟫ = P

Show details

fun {α} P => rfl

Complexity: 25 (size of the value term)

Dependencies: instToSeqList

Lean core dependencies: Eq, List, rfl

Used by: (none)

«term⟪_⟫»

A sequence written as \(a_1, \dots, a_n\), mixing single items with stretches standing for many: whatever entry is a list is spliced in, and whatever entry is a single item contributes just itself.

def «term⟪_⟫» : ParserDescr

Show details

| «term⟪_⟫» =
  ParserDescr.node `«term⟪_⟫» 1024
    (ParserDescr.binary `andthen
      (ParserDescr.binary `andthen (ParserDescr.symbol "⟪")
        ((ParserDescr.cat `term 0).sepBy "," (ParserDescr.symbol ", ")))
      (ParserDescr.symbol "⟫"))

Complexity: 61 (size of the value term)

Outer dependencies: (none)

Lean core dependencies: Lean.Name.mkStr1, Lean.ParserDescr, Nat

Used by: (none)

unexpandToSeq

Print a lone entry back as a one-element sequence.

def unexpandToSeq : PrettyPrinter.Unexpander

Show details

| unexpandToSeq x✝ =
  if x✝.isOfKind `Lean.Parser.Term.app = true then
    have __discr := x✝.getArg 0;
    have __discr := x✝.getArg 1;
    if __discr.matchesNull 1 = true then
      have __discr := __discr.getArg 0;
      have x := { raw := __discr };
      do
      let info ← MonadRef.mkInfoFromRefPos
      let _ ← getCurrMacroScope
      let _ ← MonadQuotation.getContext
      pure
          {
              raw :=
                Syntax.node3 info `«term⟪_⟫» (Syntax.atom info "⟪") (Syntax.node1 info `null x.raw)
                  (Syntax.atom info "⟫") }.raw
    else
      have __discr := x✝.getArg 1;
      throw ()
  else
    have __discr := x✝;
    throw ()

Complexity: 490 (size of the value term)

Outer dependencies: (none)

Used by: (none)

unexpandSeqAppend

Print two adjacent sequences back as one, so a whole sequence prints as it was written.

def unexpandSeqAppend : PrettyPrinter.Unexpander

Show details

| unexpandSeqAppend x✝ =
  if x✝.isOfKind `Lean.Parser.Term.app = true then
    have __discr := x✝.getArg 0;
    have __discr := x✝.getArg 1;
    if __discr.matchesNull 2 = true then
      have __discr_1 := __discr.getArg 0;
      if __discr_1.isOfKind `«term⟪_⟫» = true then
        have __discr_2 := __discr_1.getArg 0;
        have __discr_3 := __discr_1.getArg 1;
        have __discr_4 := __discr_1.getArg 2;
        have __discr_5 := __discr.getArg 1;
        if __discr_5.isOfKind `«term⟪_⟫» = true then
          have __discr := __discr_5.getArg 0;
          have __discr := __discr_5.getArg 1;
          have __discr_6 := __discr_5.getArg 2;
          have ys := { elemsAndSeps := __discr.getArgs };
          have xs := { elemsAndSeps := __discr_3.getArgs };
          have entries := xs.getElems ++ ys.getElems;
          do
          let info ← MonadRef.mkInfoFromRefPos
          let _ ← getCurrMacroScope
          let _ ← MonadQuotation.getContext
          pure
              {
                  raw :=
                    Syntax.node3 info `«term⟪_⟫» (Syntax.atom info "⟪")
                      (Syntax.node info `null
                        (#[].append (Syntax.TSepArray.ofElems entries).elemsAndSeps))
                      (Syntax.atom info "⟫") }.raw
        else
          have __discr := __discr.getArg 1;
          throw ()
      else
        have __discr_2 := __discr.getArg 0;
        have __discr := __discr.getArg 1;
        throw ()
    else
      have __discr := x✝.getArg 1;
      throw ()
  else
    have __discr := x✝;
    throw ()

Complexity: 976 (size of the value term)

Outer dependencies: (none)

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitiontheoremdeclared elsewheredependencyproof dependency

legend