replay.txt

Content-Length: 4690

{"jsonrpc":"2.0","id":0,"method":"initialize","params":{"processId":1897,"clientInfo":{"name":"Visual Studio Code","version":"1.54.2"},"locale":"en-us","rootPath":"/data/Projects/Lean/debuglean4","rootUri":"file:///data/Projects/Lean/debuglean4","capabilities":{"workspace":{"applyEdit":true,"workspaceEdit":{"documentChanges":true,"resourceOperations":["create","rename","delete"],"failureHandling":"textOnlyTransactional","normalizesLineEndings":true,"changeAnnotationSupport":{"groupsOnLabel":true}},"didChangeConfiguration":{"dynamicRegistration":true},"didChangeWatchedFiles":{"dynamicRegistration":true},"symbol":{"dynamicRegistration":true,"symbolKind":{"valueSet":[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26]},"tagSupport":{"valueSet":[1]}},"codeLens":{"refreshSupport":true},"executeCommand":{"dynamicRegistration":true},"configuration":true,"workspaceFolders":true,"semanticTokens":{"refreshSupport":true},"fileOperations":{"dynamicRegistration":true,"didCreate":true,"didRename":true,"didDelete":true,"willCreate":true,"willRename":true,"willDelete":true}},"textDocument":{"publishDiagnostics":{"relatedInformation":true,"versionSupport":false,"tagSupport":{"valueSet":[1,2]},"codeDescriptionSupport":true,"dataSupport":true},"synchronization":{"dynamicRegistration":true,"willSave":true,"willSaveWaitUntil":true,"didSave":true},"completion":{"dynamicRegistration":true,"contextSupport":true,"completionItem":{"snippetSupport":true,"commitCharactersSupport":true,"documentationFormat":["markdown","plaintext"],"deprecatedSupport":true,"preselectSupport":true,"tagSupport":{"valueSet":[1]},"insertReplaceSupport":true,"resolveSupport":{"properties":["documentation","detail","additionalTextEdits"]},"insertTextModeSupport":{"valueSet":[1,2]}},"completionItemKind":{"valueSet":[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25]}},"hover":{"dynamicRegistration":true,"contentFormat":["markdown","plaintext"]},"signatureHelp":{"dynamicRegistration":true,"signatureInformation":{"documentationFormat":["markdown","plaintext"],"parameterInformation":{"labelOffsetSupport":true},"activeParameterSupport":true},"contextSupport":true},"definition":{"dynamicRegistration":true,"linkSupport":true},"references":{"dynamicRegistration":true},"documentHighlight":{"dynamicRegistration":true},"documentSymbol":{"dynamicRegistration":true,"symbolKind":{"valueSet":[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26]},"hierarchicalDocumentSymbolSupport":true,"tagSupport":{"valueSet":[1]},"labelSupport":true},"codeAction":{"dynamicRegistration":true,"isPreferredSupport":true,"disabledSupport":true,"dataSupport":true,"resolveSupport":{"properties":["edit"]},"codeActionLiteralSupport":{"codeActionKind":{"valueSet":["","quickfix","refactor","refactor.extract","refactor.inline","refactor.rewrite","source","source.organizeImports"]}},"honorsChangeAnnotations":false},"codeLens":{"dynamicRegistration":true},"formatting":{"dynamicRegistration":true},"rangeFormatting":{"dynamicRegistration":true},"onTypeFormatting":{"dynamicRegistration":true},"rename":{"dynamicRegistration":true,"prepareSupport":true,"prepareSupportDefaultBehavior":1,"honorsChangeAnnotations":true},"documentLink":{"dynamicRegistration":true,"tooltipSupport":true},"typeDefinition":{"dynamicRegistration":true,"linkSupport":true},"implementation":{"dynamicRegistration":true,"linkSupport":true},"colorProvider":{"dynamicRegistration":true},"foldingRange":{"dynamicRegistration":true,"rangeLimit":5000,"lineFoldingOnly":true},"declaration":{"dynamicRegistration":true,"linkSupport":true},"selectionRange":{"dynamicRegistration":true},"callHierarchy":{"dynamicRegistration":true},"semanticTokens":{"dynamicRegistration":true,"tokenTypes":["namespace","type","class","enum","interface","struct","typeParameter","parameter","variable","property","enumMember","event","function","method","macro","keyword","modifier","comment","string","number","regexp","operator"],"tokenModifiers":["declaration","definition","readonly","static","deprecated","abstract","async","modification","documentation","defaultLibrary"],"formats":["relative"],"requests":{"range":true,"full":{"delta":true}},"multilineTokenSupport":false,"overlappingTokenSupport":false},"linkedEditingRange":{"dynamicRegistration":true}},"window":{"showMessage":{"messageActionItem":{"additionalPropertiesSupport":true}},"showDocument":{"support":true},"workDoneProgress":true},"general":{"regularExpressions":{"engine":"ECMAScript","version":"ES2020"},"markdown":{"parser":"marked","version":"1.1.0"}}},"trace":"off","workspaceFolders":[{"uri":"file:///data/Projects/Lean/debuglean4","name":"debuglean4"}]}}Content-Length: 52

{"jsonrpc":"2.0","method":"initialized","params":{}}Content-Length: 75310

{"jsonrpc":"2.0","method":"textDocument/didOpen","params":{"textDocument":{"uri":"file:///nix/store/jl1a92vfc7d77zs9bpw1z5fsqlc2f60h-source/src/Init/Prelude.lean","languageId":"lean4","version":1,"text":"/-\nCopyright (c) 2020 Microsoft Corporation. All rights reserved.\nReleased under Apache 2.0 license as described in the file LICENSE.\nAuthors: Leonardo de Moura\n-/\nprelude\n\nuniverses u v w\n\n@[inline] def id {α : Sort u} (a : α) : α := a\n\n/- `idRhs` is an auxiliary declaration used to implement \"smart unfolding\". It is used as a marker. -/\n@[macroInline, reducible] def idRhs (α : Sort u) (a : α) : α := a\n\nabbrev Function.comp {α : Sort u} {β : Sort v} {δ : Sort w} (f : β → δ) (g : α → β) : α → δ :=\n  fun x => f (g x)\n\nabbrev Function.const {α : Sort u} (β : Sort v) (a : α) : β → α :=\n  fun x => a\n\n@[reducible] def inferInstance {α : Sort u} [i : α] : α := i\n@[reducible] def inferInstanceAs (α : Sort u) [i : α] : α := i\n\nset_option bootstrap.inductiveCheckResultingUniverse false in\ninductive PUnit : Sort u where\n  | unit : PUnit\n\n/-- An abbreviation for `PUnit.{0}`, its most common instantiation.\n    This Type should be preferred over `PUnit` where possible to avoid\n    unnecessary universe parameters. -/\nabbrev Unit : Type := PUnit\n\n@[matchPattern] abbrev Unit.unit : Unit := PUnit.unit\n\n/-- Auxiliary unsafe constant used by the Compiler when erasing proofs from code. -/\nunsafe axiom lcProof {α : Prop} : α\n\n/-- Auxiliary unsafe constant used by the Compiler to mark unreachable code. -/\nunsafe axiom lcUnreachable {α : Sort u} : α\n\ninductive True : Prop where\n  | intro : True\n\ninductive False : Prop\n\ninductive Empty : Type\n\ndef Not (a : Prop) : Prop := a → False\n\n@[macroInline] def False.elim {C : Sort u} (h : False) : C :=\n  False.rec (fun _ => C) h\n\n@[macroInline] def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : Not a) : b :=\n  False.elim (h₂ h₁)\n\ninductive Eq {α : Sort u} (a : α) : α → Prop where\n  | refl {} : Eq a a\n\nabbrev Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m : motive a) {b : α} (h : Eq a b) : motive b :=\n  Eq.rec (motive := fun α _ => motive α) m h\n\n@[matchPattern] def rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a\n\n@[simp] theorem id_eq (a : α) : Eq (id a) a := rfl\n\ntheorem Eq.subst {α : Sort u} {motive : α → Prop} {a b : α} (h₁ : Eq a b) (h₂ : motive a) : motive b :=\n  Eq.ndrec h₂ h₁\n\ntheorem Eq.symm {α : Sort u} {a b : α} (h : Eq a b) : Eq b a :=\n  h ▸ rfl\n\ntheorem Eq.trans {α : Sort u} {a b c : α} (h₁ : Eq a b) (h₂ : Eq b c) : Eq a c :=\n  h₂ ▸ h₁\n\n@[macroInline] def cast {α β : Sort u} (h : Eq α β) (a : α) : β :=\n  Eq.rec (motive := fun α _ => α) a h\n\ntheorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : Eq a₁ a₂) : Eq (f a₁) (f a₂) :=\n  h ▸ rfl\n\ntheorem congr {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ : α} (h₁ : Eq f₁ f₂) (h₂ : Eq a₁ a₂) : Eq (f₁ a₁) (f₂ a₂) :=\n  h₁ ▸ h₂ ▸ rfl\n\ntheorem congrFun {α : Sort u} {β : α → Sort v} {f g : (x : α) →  β x} (h : Eq f g) (a : α) : Eq (f a) (g a) :=\n  h ▸ rfl\n\n/-\nInitialize the Quotient Module, which effectively adds the following definitions:\n\nconstant Quot {α : Sort u} (r : α → α → Prop) : Sort u\n\nconstant Quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : Quot r\n\nconstant Quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) :\n  (∀ a b : α, r a b → Eq (f a) (f b)) → Quot r → β\n\nconstant Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} :\n  (∀ a : α, β (Quot.mk r a)) → ∀ q : Quot r, β q\n-/\ninit_quot\n\ninductive HEq {α : Sort u} (a : α) : {β : Sort u} → β → Prop where\n  | refl {} : HEq a a\n\n@[matchPattern] def HEq.rfl {α : Sort u} {a : α} : HEq a a :=\n  HEq.refl a\n\ntheorem eqOfHEq {α : Sort u} {a a' : α} (h : HEq a a') : Eq a a' :=\n  have (α β : Sort u) → (a : α) → (b : β) → HEq a b → (h : Eq α β) → Eq (cast h a) b from\n    fun α β a b h₁ =>\n      HEq.rec (motive := fun {β} (b : β) (h : HEq a b) => (h₂ : Eq α β) → Eq (cast h₂ a) b)\n        (fun (h₂ : Eq α α) => rfl)\n        h₁\n  this α α a a' h rfl\n\nstructure Prod (α : Type u) (β : Type v) where\n  fst : α\n  snd : β\n\nattribute [unbox] Prod\n\n/-- Similar to `Prod`, but `α` and `β` can be propositions.\n   We use this Type internally to automatically generate the brecOn recursor. -/\nstructure PProd (α : Sort u) (β : Sort v) where\n  fst : α\n  snd : β\n\n/-- Similar to `Prod`, but `α` and `β` are in the same universe. -/\nstructure MProd (α β : Type u) where\n  fst : α\n  snd : β\n\nstructure And (a b : Prop) : Prop where\n  intro :: (left : a) (right : b)\n\ninductive Or (a b : Prop) : Prop where\n  | inl (h : a) : Or a b\n  | inr (h : b) : Or a b\n\ninductive Bool : Type where\n  | false : Bool\n  | true : Bool\n\nexport Bool (false true)\n\n/- Remark: Subtype must take a Sort instead of Type because of the axiom strongIndefiniteDescription. -/\nstructure Subtype {α : Sort u} (p : α → Prop) where\n  val : α\n  property : p val\n\n/-- Gadget for optional parameter support. -/\n@[reducible] def optParam (α : Sort u) (default : α) : Sort u := α\n\n/-- Gadget for marking output parameters in type classes. -/\n@[reducible] def outParam (α : Sort u) : Sort u := α\n\n/-- Auxiliary Declaration used to implement the notation (a : α) -/\n@[reducible] def typedExpr (α : Sort u) (a : α) : α := a\n\n/-- Auxiliary Declaration used to implement the named patterns `x@p` -/\n@[reducible] def namedPattern {α : Sort u} (x a : α) : α := a\n\n/- Auxiliary axiom used to implement `sorry`. -/\n@[extern \"lean_sorry\", neverExtract]\naxiom sorryAx (α : Sort u) (synthetic := true) : α\n\ntheorem eqFalseOfNeTrue : {b : Bool} → Not (Eq b true) → Eq b false\n  | true, h => False.elim (h rfl)\n  | false, h => rfl\n\ntheorem eqTrueOfNeFalse : {b : Bool} → Not (Eq b false) → Eq b true\n  | true, h => rfl\n  | false, h => False.elim (h rfl)\n\ntheorem neFalseOfEqTrue : {b : Bool} → Eq b true → Not (Eq b false)\n  | true, _  => fun h => Bool.noConfusion h\n  | false, h => Bool.noConfusion h\n\ntheorem neTrueOfEqFalse : {b : Bool} → Eq b false → Not (Eq b true)\n  | true, h  => Bool.noConfusion h\n  | false, _ => fun h => Bool.noConfusion h\n\nclass Inhabited (α : Sort u) where\n  mk {} :: (default : α)\n\nconstant arbitrary [Inhabited α] : α :=\n  Inhabited.default\n\ninstance : Inhabited (Sort u) where\n  default := PUnit\n\ninstance (α : Sort u) {β : Sort v} [Inhabited β] : Inhabited (α → β) where\n  default := fun _ => arbitrary\n\ninstance (α : Sort u) {β : α → Sort v} [(a : α) → Inhabited (β a)] : Inhabited ((a : α) → β a) where\n  default := fun _ => arbitrary\n\n/-- Universe lifting operation from Sort to Type -/\nstructure PLift (α : Sort u) : Type u where\n  up :: (down : α)\n\n/- Bijection between α and PLift α -/\ntheorem PLift.upDown {α : Sort u} : ∀ (b : PLift α), Eq (up (down b)) b\n  | up a => rfl\n\ntheorem PLift.downUp {α : Sort u} (a : α) : Eq (down (up a)) a :=\n  rfl\n\n/- Pointed types -/\nstructure PointedType where\n  (type : Type u)\n  (val : type)\n\ninstance : Inhabited PointedType.{u} where\n  default := { type := PUnit.{u+1}, val := ⟨⟩ }\n\n/-- Universe lifting operation -/\nstructure ULift.{r, s} (α : Type s) : Type (max s r) where\n  up :: (down : α)\n\n/- Bijection between α and ULift.{v} α -/\ntheorem ULift.upDown {α : Type u} : ∀ (b : ULift.{v} α), Eq (up (down b)) b\n  | up a => rfl\n\ntheorem ULift.downUp {α : Type u} (a : α) : Eq (down (up.{v} a)) a :=\n  rfl\n\nclass inductive Decidable (p : Prop) where\n  | isFalse (h : Not p) : Decidable p\n  | isTrue  (h : p) : Decidable p\n\n@[inlineIfReduce, nospecialize] def Decidable.decide (p : Prop) [h : Decidable p] : Bool :=\n  Decidable.casesOn (motive := fun _ => Bool) h (fun _ => false) (fun _ => true)\n\nexport Decidable (isTrue isFalse decide)\n\nabbrev DecidablePred {α : Sort u} (r : α → Prop) :=\n  (a : α) → Decidable (r a)\n\nabbrev DecidableRel {α : Sort u} (r : α → α → Prop) :=\n  (a b : α) → Decidable (r a b)\n\nabbrev DecidableEq (α : Sort u) :=\n  (a b : α) → Decidable (Eq a b)\n\ndef decEq {α : Sort u} [s : DecidableEq α] (a b : α) : Decidable (Eq a b) :=\n  s a b\n\ntheorem decideEqTrue : {p : Prop} → [s : Decidable p] → p → Eq (decide p) true\n  | _, isTrue  _, _   => rfl\n  | _, isFalse h₁, h₂ => absurd h₂ h₁\n\ntheorem decideEqFalse : {p : Prop} → [s : Decidable p] → Not p → Eq (decide p) false\n  | _, isTrue  h₁, h₂ => absurd h₁ h₂\n  | _, isFalse h, _   => rfl\n\ntheorem ofDecideEqTrue {p : Prop} [s : Decidable p] : Eq (decide p) true → p := fun h =>\n  match s with\n  | isTrue  h₁ => h₁\n  | isFalse h₁ => absurd h (neTrueOfEqFalse (decideEqFalse h₁))\n\ntheorem ofDecideEqFalse {p : Prop} [s : Decidable p] : Eq (decide p) false → Not p := fun h =>\n  match s with\n  | isTrue  h₁ => absurd h (neFalseOfEqTrue (decideEqTrue h₁))\n  | isFalse h₁ => h₁\n\n@[inline] instance : DecidableEq Bool :=\n  fun a b => match a, b with\n   | false, false => isTrue rfl\n   | false, true  => isFalse (fun h => Bool.noConfusion h)\n   | true, false  => isFalse (fun h => Bool.noConfusion h)\n   | true, true   => isTrue rfl\n\nclass BEq (α : Type u) where\n  beq : α → α → Bool\n\nopen BEq (beq)\n\ninstance {α : Type u} [DecidableEq α] : BEq α where\n  beq a b := decide (Eq a b)\n\n-- We use \"dependent\" if-then-else to be able to communicate the if-then-else condition\n-- to the branches\n@[macroInline] def dite {α : Sort u} (c : Prop) [h : Decidable c] (t : c → α) (e : Not c → α) : α :=\n  Decidable.casesOn (motive := fun _ => α) h e t\n\n/- if-then-else -/\n\n@[macroInline] def ite {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α :=\n  Decidable.casesOn (motive := fun _ => α) h (fun _ => e) (fun _ => t)\n\n@[macroInline] instance {p q} [dp : Decidable p] [dq : Decidable q] : Decidable (And p q) :=\n  match dp with\n  | isTrue  hp =>\n    match dq with\n    | isTrue hq  => isTrue ⟨hp, hq⟩\n    | isFalse hq => isFalse (fun h => hq (And.right h))\n  | isFalse hp =>\n    isFalse (fun h => hp (And.left h))\n\n@[macroInline] instance {p q} [dp : Decidable p] [dq : Decidable q] : Decidable (Or p q) :=\n  match dp with\n  | isTrue  hp => isTrue (Or.inl hp)\n  | isFalse hp =>\n    match dq with\n    | isTrue hq  => isTrue (Or.inr hq)\n    | isFalse hq =>\n      isFalse fun h => match h with\n        | Or.inl h => hp h\n        | Or.inr h => hq h\n\ninstance {p} [dp : Decidable p] : Decidable (Not p) :=\n  match dp with\n  | isTrue hp  => isFalse (absurd hp)\n  | isFalse hp => isTrue hp\n\n/- Boolean operators -/\n\n@[macroInline] def cond {α : Type u} (c : Bool) (x y : α) : α :=\n  match c with\n  | true  => x\n  | false => y\n\n@[macroInline] def or (x y : Bool) : Bool :=\n  match x with\n  | true  => true\n  | false => y\n\n@[macroInline] def and (x y : Bool) : Bool :=\n  match x with\n  | false => false\n  | true  => y\n\n@[inline] def not : Bool → Bool\n  | true  => false\n  | false => true\n\ninductive Nat where\n  | zero : Nat\n  | succ (n : Nat) : Nat\n\ninstance : Inhabited Nat where\n  default := Nat.zero\n\n/- For numeric literals notation -/\nclass OfNat (α : Type u) (n : Nat) where\n  ofNat : α\n\n@[defaultInstance 100] /- low prio -/\ninstance (n : Nat) : OfNat Nat n where\n  ofNat := n\n\nclass HasLessEq (α : Type u) where LessEq : α → α → Prop\nclass HasLess   (α : Type u) where Less : α → α → Prop\n\nexport HasLess (Less)\nexport HasLessEq (LessEq)\n\nclass HAdd (α : Type u) (β : Type v) (γ : outParam (Type w)) where\n  hAdd : α → β → γ\n\nclass HSub (α : Type u) (β : Type v) (γ : outParam (Type w)) where\n  hSub : α → β → γ\n\nclass HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where\n  hMul : α → β → γ\n\nclass HDiv (α : Type u) (β : Type v) (γ : outParam (Type w)) where\n  hDiv : α → β → γ\n\nclass HMod (α : Type u) (β : Type v) (γ : outParam (Type w)) where\n  hMod : α → β → γ\n\nclass HPow (α : Type u) (β : Type v) (γ : outParam (Type w)) where\n  hPow : α → β → γ\n\nclass HAppend (α : Type u) (β : Type v) (γ : outParam (Type w)) where\n  hAppend : α → β → γ\n\nclass HOrElse (α : Type u) (β : Type v) (γ : outParam (Type w)) where\n  hOrElse : α → β → γ\n\nclass HAndThen (α : Type u) (β : Type v) (γ : outParam (Type w)) where\n  hAndThen : α → β → γ\n\nclass HAnd (α : Type u) (β : Type v) (γ : outParam (Type w)) where\n  hAnd : α → β → γ\n\nclass HXor (α : Type u) (β : Type v) (γ : outParam (Type w)) where\n  hXor : α → β → γ\n\nclass HOr (α : Type u) (β : Type v) (γ : outParam (Type w)) where\n  hOr : α → β → γ\n\nclass HShiftLeft (α : Type u) (β : Type v) (γ : outParam (Type w)) where\n  hShiftLeft : α → β → γ\n\nclass HShiftRight (α : Type u) (β : Type v) (γ : outParam (Type w)) where\n  hShiftRight : α → β → γ\n\nclass Add (α : Type u) where\n  add : α → α → α\n\nclass Sub (α : Type u) where\n  sub : α → α → α\n\nclass Mul (α : Type u) where\n  mul : α → α → α\n\nclass Neg (α : Type u) where\n  neg : α → α\n\nclass Div (α : Type u) where\n  div : α → α → α\n\nclass Mod (α : Type u) where\n  mod : α → α → α\n\nclass Pow (α : Type u) where\n  pow : α → α → α\n\nclass Append (α : Type u) where\n  append : α → α → α\n\nclass OrElse (α : Type u) where\n  orElse  : α → α → α\n\nclass AndThen (α : Type u) where\n  andThen : α → α → α\n\nclass AndOp (α : Type u) where\n  and : α → α → α\n\nclass Xor (α : Type u) where\n  xor : α → α → α\n\nclass OrOp (α : Type u) where\n  or : α → α → α\n\nclass Complement (α : Type u) where\n  complement : α → α\n\nclass ShiftLeft (α : Type u) where\n  shiftLeft : α → α → α\n\nclass ShiftRight (α : Type u) where\n  shiftRight : α → α → α\n\n@[defaultInstance]\ninstance [Add α] : HAdd α α α where\n  hAdd a b := Add.add a b\n\n@[defaultInstance]\ninstance [Sub α] : HSub α α α where\n  hSub a b := Sub.sub a b\n\n@[defaultInstance]\ninstance [Mul α] : HMul α α α where\n  hMul a b := Mul.mul a b\n\n@[defaultInstance]\ninstance [Div α] : HDiv α α α where\n  hDiv a b := Div.div a b\n\n@[defaultInstance]\ninstance [Mod α] : HMod α α α where\n  hMod a b := Mod.mod a b\n\n@[defaultInstance]\ninstance [Pow α] : HPow α α α where\n  hPow a b := Pow.pow a b\n\n@[defaultInstance]\ninstance [Append α] : HAppend α α α where\n  hAppend a b := Append.append a b\n\n@[defaultInstance]\ninstance [OrElse α] : HOrElse α α α where\n  hOrElse a b := OrElse.orElse a b\n\n@[defaultInstance]\ninstance [AndThen α] : HAndThen α α α where\n  hAndThen a b := AndThen.andThen a b\n\n@[defaultInstance]\ninstance [AndOp α] : HAnd α α α where\n  hAnd a b := AndOp.and a b\n\n@[defaultInstance]\ninstance [Xor α] : HXor α α α where\n  hXor a b := Xor.xor a b\n\n@[defaultInstance]\ninstance [OrOp α] : HOr α α α where\n  hOr a b := OrOp.or a b\n\n@[defaultInstance]\ninstance [ShiftLeft α] : HShiftLeft α α α where\n  hShiftLeft a b := ShiftLeft.shiftLeft a b\n\n@[defaultInstance]\ninstance [ShiftRight α] : HShiftRight α α α where\n  hShiftRight a b := ShiftRight.shiftRight a b\n\nopen HAdd (hAdd)\nopen HMul (hMul)\nopen HPow (hPow)\nopen HAppend (hAppend)\n\n@[reducible] def GreaterEq {α : Type u} [HasLessEq α] (a b : α) : Prop := LessEq b a\n@[reducible] def Greater {α : Type u} [HasLess α] (a b : α) : Prop     := Less b a\n\nset_option bootstrap.genMatcherCode false in\n@[extern \"lean_nat_add\"]\nprotected def Nat.add : (@& Nat) → (@& Nat) → Nat\n  | a, Nat.zero   => a\n  | a, Nat.succ b => Nat.succ (Nat.add a b)\n\ninstance : Add Nat where\n  add := Nat.add\n\n/- We mark the following definitions as pattern to make sure they can be used in recursive equations,\n   and reduced by the equation Compiler. -/\nattribute [matchPattern] Nat.add Add.add HAdd.hAdd Neg.neg\n\nset_option bootstrap.genMatcherCode false in\n@[extern \"lean_nat_mul\"]\nprotected def Nat.mul : (@& Nat) → (@& Nat) → Nat\n  | a, 0          => 0\n  | a, Nat.succ b => Nat.add (Nat.mul a b) a\n\ninstance : Mul Nat where\n  mul := Nat.mul\n\nset_option bootstrap.genMatcherCode false in\n@[extern \"lean_nat_pow\"]\nprotected def Nat.pow (m : @& Nat) : (@& Nat) → Nat\n  | 0      => 1\n  | succ n => Nat.mul (Nat.pow m n) m\n\ninstance : Pow Nat where\n  pow := Nat.pow\n\nset_option bootstrap.genMatcherCode false in\n@[extern \"lean_nat_dec_eq\"]\ndef Nat.beq : (@& Nat) → (@& Nat) → Bool\n  | zero,   zero   => true\n  | zero,   succ m => false\n  | succ n, zero   => false\n  | succ n, succ m => beq n m\n\ntheorem Nat.eqOfBeqEqTrue : {n m : Nat} → Eq (beq n m) true → Eq n m\n  | zero,   zero,   h => rfl\n  | zero,   succ m, h => Bool.noConfusion h\n  | succ n, zero,   h => Bool.noConfusion h\n  | succ n, succ m, h =>\n    have Eq (beq n m) true from h\n    have Eq n m from eqOfBeqEqTrue this\n    this ▸ rfl\n\ntheorem Nat.neOfBeqEqFalse : {n m : Nat} → Eq (beq n m) false → Not (Eq n m)\n  | zero,   zero,   h₁, h₂ => Bool.noConfusion h₁\n  | zero,   succ m, h₁, h₂ => Nat.noConfusion h₂\n  | succ n, zero,   h₁, h₂ => Nat.noConfusion h₂\n  | succ n, succ m, h₁, h₂ =>\n    have Eq (beq n m) false from h₁\n    Nat.noConfusion h₂ (fun h₂ => absurd h₂ (neOfBeqEqFalse this))\n\n@[extern \"lean_nat_dec_eq\"]\nprotected def Nat.decEq (n m : @& Nat) : Decidable (Eq n m) :=\n  match h:beq n m with\n  | true  => isTrue (eqOfBeqEqTrue h)\n  | false => isFalse (neOfBeqEqFalse h)\n\n@[inline] instance : DecidableEq Nat := Nat.decEq\n\nset_option bootstrap.genMatcherCode false in\n@[extern \"lean_nat_dec_le\"]\ndef Nat.ble : @& Nat → @& Nat → Bool\n  | zero,   zero   => true\n  | zero,   succ m => true\n  | succ n, zero   => false\n  | succ n, succ m => ble n m\n\nprotected def Nat.le (n m : Nat) : Prop :=\n  Eq (ble n m) true\n\ninstance : HasLessEq Nat where\n  LessEq := Nat.le\n\nprotected def Nat.lt (n m : Nat) : Prop :=\n  Nat.le (succ n) m\n\ninstance : HasLess Nat where\n  Less := Nat.lt\n\ntheorem Nat.notSuccLeZero : ∀ (n : Nat), LessEq (succ n) 0 → False\n  | 0,      h => nomatch h\n  | succ n, h => nomatch h\n\ntheorem Nat.notLtZero (n : Nat) : Not (Less n 0) :=\n  notSuccLeZero n\n\n@[extern \"lean_nat_dec_le\"]\ninstance Nat.decLe (n m : @& Nat) : Decidable (LessEq n m) :=\n  decEq (Nat.ble n m) true\n\n@[extern \"lean_nat_dec_lt\"]\ninstance Nat.decLt (n m : @& Nat) : Decidable (Less n m) :=\n  decLe (succ n) m\n\ntheorem Nat.zeroLe : (n : Nat) → LessEq 0 n\n  | zero   => rfl\n  | succ n => rfl\n\ntheorem Nat.succLeSucc {n m : Nat} (h : LessEq n m) : LessEq (succ n) (succ m) :=\n  h\n\ntheorem Nat.zeroLtSucc (n : Nat) : Less 0 (succ n) :=\n  succLeSucc (zeroLe n)\n\ntheorem Nat.leStep : {n m : Nat} → LessEq n m → LessEq n (succ m)\n  | zero,   zero,   h => rfl\n  | zero,   succ n, h => rfl\n  | succ n, zero,   h => Bool.noConfusion h\n  | succ n, succ m, h =>\n    have LessEq n m from h\n    have LessEq n (succ m) from leStep this\n    succLeSucc this\n\nset_option pp.raw true\nprotected theorem Nat.leTrans : {n m k : Nat} → LessEq n m → LessEq m k → LessEq n k\n  | zero,   m,      k,      h₁, h₂ => zeroLe _\n  | succ n, zero,   k,      h₁, h₂ => Bool.noConfusion h₁\n  | succ n, succ m, zero,   h₁, h₂ => Bool.noConfusion h₂\n  | succ n, succ m, succ k, h₁, h₂ =>\n    have h₁' : LessEq n m from h₁\n    have h₂' : LessEq m k from h₂\n    show LessEq n k from\n    Nat.leTrans h₁' h₂'\n\nprotected theorem Nat.ltTrans {n m k : Nat} (h₁ : Less n m) : Less m k → Less n k :=\n  Nat.leTrans (leStep h₁)\n\ntheorem Nat.leSucc : (n : Nat) → LessEq n (succ n)\n  | zero   => rfl\n  | succ n => leSucc n\n\ntheorem Nat.leSuccOfLe {n m : Nat} (h : LessEq n m) : LessEq n (succ m) :=\n  Nat.leTrans h (leSucc m)\n\nprotected theorem Nat.eqOrLtOfLe : {n m: Nat} → LessEq n m → Or (Eq n m) (Less n m)\n  | zero,   zero,   h => Or.inl rfl\n  | zero,   succ n, h => Or.inr (zeroLe n)\n  | succ n, zero,   h => Bool.noConfusion h\n  | succ n, succ m, h =>\n    have LessEq n m from h\n    match Nat.eqOrLtOfLe this with\n    | Or.inl h => Or.inl (h ▸ rfl)\n    | Or.inr h => Or.inr (succLeSucc h)\n\nprotected def Nat.leRefl : (n : Nat) → LessEq n n\n  | zero   => rfl\n  | succ n => Nat.leRefl n\n\nprotected theorem Nat.ltOrGe (n m : Nat) : Or (Less n m) (GreaterEq n m) :=\n  match m with\n  | zero   => Or.inr (zeroLe n)\n  | succ m =>\n    match Nat.ltOrGe n m with\n    | Or.inl h => Or.inl (leSuccOfLe h)\n    | Or.inr h =>\n      match Nat.eqOrLtOfLe h with\n      | Or.inl h1 => Or.inl (h1 ▸ Nat.leRefl _)\n      | Or.inr h1 => Or.inr h1\n\nprotected theorem Nat.leAntisymm : {n m : Nat} → LessEq n m → LessEq m n → Eq n m\n  | zero,   zero,   h₁, h₂ => rfl\n  | succ n, zero,   h₁, h₂ => Bool.noConfusion h₁\n  | zero,   succ m, h₁, h₂ => Bool.noConfusion h₂\n  | succ n, succ m, h₁, h₂ =>\n    have h₁' : LessEq n m from h₁\n    have h₂' : LessEq m n from h₂\n    (Nat.leAntisymm h₁' h₂') ▸ rfl\n\nprotected theorem Nat.ltOfLeOfNe {n m : Nat} (h₁ : LessEq n m) (h₂ : Not (Eq n m)) : Less n m :=\n  match Nat.ltOrGe n m with\n  | Or.inl h₃ => h₃\n  | Or.inr h₃ => absurd (Nat.leAntisymm h₁ h₃) h₂\n\nset_option bootstrap.genMatcherCode false in\n@[extern c inline \"lean_nat_sub(#1, lean_box(1))\"]\ndef Nat.pred : (@& Nat) → Nat\n  | 0      => 0\n  | succ a => a\n\nset_option bootstrap.genMatcherCode false in\n@[extern \"lean_nat_sub\"]\nprotected def Nat.sub : (@& Nat) → (@& Nat) → Nat\n  | a, 0      => a\n  | a, succ b => pred (Nat.sub a b)\n\ninstance : Sub Nat where\n  sub := Nat.sub\n\ntheorem Nat.predLePred : {n m : Nat} → LessEq n m → LessEq (pred n) (pred m)\n  | zero,   zero,   h => rfl\n  | zero,   succ n, h => zeroLe n\n  | succ n, zero,   h => Bool.noConfusion h\n  | succ n, succ m, h => h\n\ntheorem Nat.leOfSuccLeSucc {n m : Nat} : LessEq (succ n) (succ m) → LessEq n m :=\n  predLePred\n\ntheorem Nat.leOfLtSucc {m n : Nat} : Less m (succ n) → LessEq m n :=\n  leOfSuccLeSucc\n\n@[extern \"lean_system_platform_nbits\"] constant System.Platform.getNumBits : Unit → Subtype fun (n : Nat) => Or (Eq n 32) (Eq n 64) :=\n  fun _ => ⟨64, Or.inr rfl⟩ -- inhabitant\n\ndef System.Platform.numBits : Nat :=\n  (getNumBits ()).val\n\ntheorem System.Platform.numBitsEq : Or (Eq numBits 32) (Eq numBits 64) :=\n  (getNumBits ()).property\n\nstructure Fin (n : Nat) where\n  val  : Nat\n  isLt : Less val n\n\ntheorem Fin.eqOfVeq {n} : ∀ {i j : Fin n}, Eq i.val j.val → Eq i j\n  | ⟨v, h⟩, ⟨_, _⟩, rfl => rfl\n\ntheorem Fin.veqOfEq {n} {i j : Fin n} (h : Eq i j) : Eq i.val j.val :=\n  h ▸ rfl\n\ntheorem Fin.neOfVne {n} {i j : Fin n} (h : Not (Eq i.val j.val)) : Not (Eq i j) :=\n  fun h' => absurd (veqOfEq h') h\n\ninstance (n : Nat) : DecidableEq (Fin n) :=\n  fun i j =>\n    match decEq i.val j.val with\n    | isTrue h  => isTrue (Fin.eqOfVeq h)\n    | isFalse h => isFalse (Fin.neOfVne h)\n\ninstance {n} : HasLess (Fin n) where\n  Less a b := Less a.val b.val\n\ninstance {n} : HasLessEq (Fin n) where\n  LessEq a b := LessEq a.val b.val\n\ninstance Fin.decLt {n} (a b : Fin n) :  Decidable (Less a b)  := Nat.decLt ..\ninstance Fin.decLe {n} (a b : Fin n) : Decidable (LessEq a b) := Nat.decLe ..\n\ndef UInt8.size : Nat := 256\nstructure UInt8 where\n  val : Fin UInt8.size\n\nattribute [extern \"lean_uint8_of_nat_mk\"] UInt8.mk\nattribute [extern \"lean_uint8_to_nat\"] UInt8.val\n\n@[extern \"lean_uint8_of_nat\"]\ndef UInt8.ofNatCore (n : @& Nat) (h : Less n UInt8.size) : UInt8 := {\n  val := { val := n, isLt := h }\n}\n\nset_option bootstrap.genMatcherCode false in\n@[extern c inline \"#1 == #2\"]\ndef UInt8.decEq (a b : UInt8) : Decidable (Eq a b) :=\n  match a, b with\n  | ⟨n⟩, ⟨m⟩ =>\n    dite (Eq n m) (fun h => isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => UInt8.noConfusion h' (fun h' => absurd h' h)))\n\ninstance : DecidableEq UInt8 := UInt8.decEq\n\ninstance : Inhabited UInt8 where\n  default := UInt8.ofNatCore 0 (by decide)\n\ndef UInt16.size : Nat := 65536\nstructure UInt16 where\n  val : Fin UInt16.size\n\nattribute [extern \"lean_uint16_of_nat_mk\"] UInt16.mk\nattribute [extern \"lean_uint16_to_nat\"] UInt16.val\n\n@[extern \"lean_uint16_of_nat\"]\ndef UInt16.ofNatCore (n : @& Nat) (h : Less n UInt16.size) : UInt16 := {\n  val := { val := n, isLt := h }\n}\n\nset_option bootstrap.genMatcherCode false in\n@[extern c inline \"#1 == #2\"]\ndef UInt16.decEq (a b : UInt16) : Decidable (Eq a b) :=\n  match a, b with\n  | ⟨n⟩, ⟨m⟩ =>\n    dite (Eq n m) (fun h => isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => UInt16.noConfusion h' (fun h' => absurd h' h)))\n\ninstance : DecidableEq UInt16 := UInt16.decEq\n\ninstance : Inhabited UInt16 where\n  default := UInt16.ofNatCore 0 (by decide)\n\ndef UInt32.size : Nat := 4294967296\nstructure UInt32 where\n  val : Fin UInt32.size\n\nattribute [extern \"lean_uint32_of_nat_mk\"] UInt32.mk\nattribute [extern \"lean_uint32_to_nat\"] UInt32.val\n\n@[extern \"lean_uint32_of_nat\"]\ndef UInt32.ofNatCore (n : @& Nat) (h : Less n UInt32.size) : UInt32 := {\n  val := { val := n, isLt := h }\n}\n\n@[extern \"lean_uint32_to_nat\"]\ndef UInt32.toNat (n : UInt32) : Nat := n.val.val\n\nset_option bootstrap.genMatcherCode false in\n@[extern c inline \"#1 == #2\"]\ndef UInt32.decEq (a b : UInt32) : Decidable (Eq a b) :=\n  match a, b with\n  | ⟨n⟩, ⟨m⟩ =>\n    dite (Eq n m) (fun h => isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => UInt32.noConfusion h' (fun h' => absurd h' h)))\n\ninstance : DecidableEq UInt32 := UInt32.decEq\n\ninstance : Inhabited UInt32 where\n  default := UInt32.ofNatCore 0 (by decide)\n\ninstance : HasLess UInt32 where\n  Less a b := Less a.val b.val\n\ninstance : HasLessEq UInt32 where\n  LessEq a b := LessEq a.val b.val\n\nset_option bootstrap.genMatcherCode false in\n@[extern c inline \"#1 < #2\"]\ndef UInt32.decLt (a b : UInt32) : Decidable (Less a b) :=\n  match a, b with\n  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (Less n m))\n\nset_option bootstrap.genMatcherCode false in\n@[extern c inline \"#1 <= #2\"]\ndef UInt32.decLe (a b : UInt32) : Decidable (LessEq a b) :=\n  match a, b with\n  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (LessEq n m))\n\ninstance (a b : UInt32) : Decidable (Less a b) := UInt32.decLt a b\ninstance (a b : UInt32) : Decidable (LessEq a b) := UInt32.decLe a b\n\ndef UInt64.size : Nat := 18446744073709551616\nstructure UInt64 where\n  val : Fin UInt64.size\n\nattribute [extern \"lean_uint64_of_nat_mk\"] UInt64.mk\nattribute [extern \"lean_uint64_to_nat\"] UInt64.val\n\n@[extern \"lean_uint64_of_nat\"]\ndef UInt64.ofNatCore (n : @& Nat) (h : Less n UInt64.size) : UInt64 := {\n  val := { val := n, isLt := h }\n}\n\nset_option bootstrap.genMatcherCode false in\n@[extern c inline \"#1 == #2\"]\ndef UInt64.decEq (a b : UInt64) : Decidable (Eq a b) :=\n  match a, b with\n  | ⟨n⟩, ⟨m⟩ =>\n    dite (Eq n m) (fun h => isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => UInt64.noConfusion h' (fun h' => absurd h' h)))\n\ninstance : DecidableEq UInt64 := UInt64.decEq\n\ninstance : Inhabited UInt64 where\n  default := UInt64.ofNatCore 0 (by decide)\n\ndef USize.size : Nat := hPow 2 System.Platform.numBits\n\ntheorem usizeSzEq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) :=\n  show Or (Eq (hPow 2 System.Platform.numBits) 4294967296) (Eq (hPow 2 System.Platform.numBits) 18446744073709551616) from\n  match System.Platform.numBits, System.Platform.numBitsEq with\n  | _, Or.inl rfl => Or.inl (by decide)\n  | _, Or.inr rfl => Or.inr (by decide)\n\nstructure USize where\n  val : Fin USize.size\n\nattribute [extern \"lean_usize_of_nat_mk\"] USize.mk\nattribute [extern \"lean_usize_to_nat\"] USize.val\n\n@[extern \"lean_usize_of_nat\"]\ndef USize.ofNatCore (n : @& Nat) (h : Less n USize.size) : USize := {\n  val := { val := n, isLt := h }\n}\n\nset_option bootstrap.genMatcherCode false in\n@[extern c inline \"#1 == #2\"]\ndef USize.decEq (a b : USize) : Decidable (Eq a b) :=\n  match a, b with\n  | ⟨n⟩, ⟨m⟩ =>\n    dite (Eq n m) (fun h =>isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => USize.noConfusion h' (fun h' => absurd h' h)))\n\ninstance : DecidableEq USize := USize.decEq\n\ninstance : Inhabited USize where\n  default := USize.ofNatCore 0 (match USize.size, usizeSzEq with\n    | _, Or.inl rfl => by decide\n    | _, Or.inr rfl => by decide)\n\n@[extern \"lean_usize_of_nat\"]\ndef USize.ofNat32 (n : @& Nat) (h : Less n 4294967296) : USize := {\n  val := {\n    val  := n,\n    isLt := match USize.size, usizeSzEq with\n      | _, Or.inl rfl => h\n      | _, Or.inr rfl => Nat.ltTrans h (by decide)\n  }\n}\n\nabbrev Nat.isValidChar (n : Nat) : Prop :=\n  Or (Less n 0xd800) (And (Less 0xdfff n) (Less n 0x110000))\n\nabbrev UInt32.isValidChar (n : UInt32) : Prop :=\n  n.toNat.isValidChar\n\n/-- The `Char` Type represents an unicode scalar value.\n    See http://www.unicode.org/glossary/#unicode_scalar_value). -/\nstructure Char where\n  val   : UInt32\n  valid : val.isValidChar\n\nprivate theorem validCharIsUInt32 {n : Nat} (h : n.isValidChar) : Less n UInt32.size :=\n  match h with\n  | Or.inl h      => Nat.ltTrans h (by decide)\n  | Or.inr ⟨_, h⟩ => Nat.ltTrans h (by decide)\n\n@[extern \"lean_uint32_of_nat\"]\nprivate def Char.ofNatAux (n : @& Nat) (h : n.isValidChar) : Char :=\n  { val := ⟨{ val := n, isLt := validCharIsUInt32 h }⟩, valid := h }\n\n@[noinline, matchPattern]\ndef Char.ofNat (n : Nat) : Char :=\n  dite (n.isValidChar)\n    (fun h => Char.ofNatAux n h)\n    (fun _ => { val := ⟨{ val := 0, isLt := by decide }⟩, valid := Or.inl (by decide) })\n\ntheorem Char.eqOfVeq : ∀ {c d : Char}, Eq c.val d.val → Eq c d\n  | ⟨v, h⟩, ⟨_, _⟩, rfl => rfl\n\ntheorem Char.veqOfEq : ∀ {c d : Char}, Eq c d → Eq c.val d.val\n  | _, _, rfl => rfl\n\ntheorem Char.neOfVne {c d : Char} (h : Not (Eq c.val d.val)) : Not (Eq c d) :=\n  fun h' => absurd (veqOfEq h') h\n\ntheorem Char.vneOfNe {c d : Char} (h : Not (Eq c d)) : Not (Eq c.val d.val) :=\n  fun h' => absurd (eqOfVeq h') h\n\ninstance : DecidableEq Char :=\n  fun c d =>\n    match decEq c.val d.val with\n    | isTrue h  => isTrue (Char.eqOfVeq h)\n    | isFalse h => isFalse (Char.neOfVne h)\n\ndef Char.utf8Size (c : Char) : UInt32 :=\n  let v := c.val\n  ite (LessEq v (UInt32.ofNatCore 0x7F (by decide)))\n    (UInt32.ofNatCore 1 (by decide))\n    (ite (LessEq v (UInt32.ofNatCore 0x7FF (by decide)))\n      (UInt32.ofNatCore 2 (by decide))\n      (ite (LessEq v (UInt32.ofNatCore 0xFFFF (by decide)))\n        (UInt32.ofNatCore 3 (by decide))\n        (UInt32.ofNatCore 4 (by decide))))\n\ninductive Option (α : Type u) where\n  | none : Option α\n  | some (val : α) : Option α\n\nattribute [unbox] Option\n\nexport Option (none some)\n\ninstance {α} : Inhabited (Option α) where\n  default := none\n\ninductive List (α : Type u) where\n  | nil : List α\n  | cons (head : α) (tail : List α) : List α\n\ninstance {α} : Inhabited (List α) where\n  default := List.nil\n\nprotected def List.hasDecEq {α: Type u} [DecidableEq α] : (a b : List α) → Decidable (Eq a b)\n  | nil,       nil       => isTrue rfl\n  | cons a as, nil       => isFalse (fun h => List.noConfusion h)\n  | nil,       cons b bs => isFalse (fun h => List.noConfusion h)\n  | cons a as, cons b bs =>\n    match decEq a b with\n    | isTrue hab  =>\n      match List.hasDecEq as bs with\n      | isTrue habs  => isTrue (hab ▸ habs ▸ rfl)\n      | isFalse nabs => isFalse (fun h => List.noConfusion h (fun _ habs => absurd habs nabs))\n    | isFalse nab => isFalse (fun h => List.noConfusion h (fun hab _ => absurd hab nab))\n\ninstance {α : Type u} [DecidableEq α] : DecidableEq (List α) := List.hasDecEq\n\n@[specialize]\ndef List.foldl {α β} (f : α → β → α) : (init : α) → List β → α\n  | a, nil      => a\n  | a, cons b l => foldl f (f a b) l\n\ndef List.set : List α → Nat → α → List α\n  | cons a as, 0,          b => cons b as\n  | cons a as, Nat.succ n, b => cons a (set as n b)\n  | nil,       _,          _ => nil\n\ndef List.lengthAux {α : Type u} : List α → Nat → Nat\n  | nil,       n => n\n  | cons a as, n => lengthAux as (Nat.succ n)\n\ndef List.length {α : Type u} (as : List α) : Nat :=\n  lengthAux as 0\n\n@[simp] theorem List.length_cons {α} (a : α) (as : List α) : Eq (cons a as).length as.length.succ :=\n  let rec aux (a : α) (as : List α) : (n : Nat) → Eq ((cons a as).lengthAux n) (as.lengthAux n).succ :=\n    match as with\n    | nil       => fun _ => rfl\n    | cons a as => fun n => aux a as n.succ\n  aux a as 0\n\ndef List.concat {α : Type u} : List α → α → List α\n  | nil,       b => cons b nil\n  | cons a as, b => cons a (concat as b)\n\ndef List.get {α : Type u} : (as : List α) → (i : Nat) → Less i as.length → α\n  | nil,       i,          h => absurd h (Nat.notLtZero _)\n  | cons a as, 0,          h => a\n  | cons a as, Nat.succ i, h =>\n    have Less i.succ as.length.succ from length_cons .. ▸ h\n    get as i (Nat.leOfSuccLeSucc this)\n\nstructure String where\n  data : List Char\n\nattribute [extern \"lean_string_mk\"] String.mk\nattribute [extern \"lean_string_data\"] String.data\n\n@[extern \"lean_string_dec_eq\"]\ndef String.decEq (s₁ s₂ : @& String) : Decidable (Eq s₁ s₂) :=\n  match s₁, s₂ with\n  | ⟨s₁⟩, ⟨s₂⟩ =>\n   dite (Eq s₁ s₂) (fun h => isTrue (congrArg _ h)) (fun h => isFalse (fun h' => String.noConfusion h' (fun h' => absurd h' h)))\n\ninstance : DecidableEq String := String.decEq\n\n/-- A byte position in a `String`. Internally, `String`s are UTF-8 encoded.\nCodepoint positions (counting the Unicode codepoints rather than bytes)\nare represented by plain `Nat`s instead.\nIndexing a `String` by a byte position is constant-time, while codepoint\npositions need to be translated internally to byte positions in linear-time. -/\nabbrev String.Pos := Nat\n\nstructure Substring where\n  str : String\n  startPos : String.Pos\n  stopPos : String.Pos\n\n@[inline] def Substring.bsize : Substring → Nat\n  | ⟨_, b, e⟩ => e.sub b\n\ndef String.csize (c : Char) : Nat :=\n  c.utf8Size.toNat\n\nprivate def String.utf8ByteSizeAux : List Char → Nat → Nat\n  | List.nil,       r => r\n  | List.cons c cs, r => utf8ByteSizeAux cs (hAdd r (csize c))\n\n@[extern \"lean_string_utf8_byte_size\"]\ndef String.utf8ByteSize : (@& String) → Nat\n  | ⟨s⟩ => utf8ByteSizeAux s 0\n\n@[inline] def String.bsize (s : String) : Nat :=\n  utf8ByteSize s\n\n@[inline] def String.toSubstring (s : String) : Substring := {\n  str := s,\n  startPos := 0,\n  stopPos  := s.bsize\n}\n\n@[extern c inline \"#3\"]\nunsafe def unsafeCast {α : Type u} {β : Type v} (a : α) : β :=\n  cast lcProof (PUnit.{v})\n\n@[neverExtract, extern \"lean_panic_fn\"]\nconstant panic {α : Type u} [Inhabited α] (msg : String) : α\n\n/-\nThe Compiler has special support for arrays.\nThey are implemented using dynamic arrays: https://en.wikipedia.org/wiki/Dynamic_array\n-/\nstructure Array (α : Type u) where\n  data : List α\n\nattribute [extern \"lean_array_data\"] Array.data\nattribute [extern \"lean_array_mk\"] Array.mk\n\n/- The parameter `c` is the initial capacity -/\n@[extern \"lean_mk_empty_array_with_capacity\"]\ndef Array.mkEmpty {α : Type u} (c : @& Nat) : Array α := {\n  data := List.nil\n}\n\ndef Array.empty {α : Type u} : Array α :=\n  mkEmpty 0\n\n@[reducible, extern \"lean_array_get_size\"]\ndef Array.size {α : Type u} (a : @& Array α) : Nat :=\n a.data.length\n\n@[extern \"lean_array_fget\"]\ndef Array.get {α : Type u} (a : @& Array α) (i : @& Fin a.size) : α :=\n  a.data.get i.val i.isLt\n\n@[inline] def Array.getD (a : Array α) (i : Nat) (v₀ : α) : α :=\n  dite (Less i a.size) (fun h => a.get ⟨i, h⟩) (fun _ => v₀)\n\n/- \"Comfortable\" version of `fget`. It performs a bound check at runtime. -/\n@[extern \"lean_array_get\"]\ndef Array.get! {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=\n  Array.getD a i arbitrary\n\ndef Array.getOp {α : Type u} [Inhabited α] (self : Array α) (idx : Nat) : α :=\n  self.get! idx\n\n@[extern \"lean_array_push\"]\ndef Array.push {α : Type u} (a : Array α) (v : α) : Array α := {\n  data := List.concat a.data v\n}\n\n@[extern \"lean_array_fset\"]\ndef Array.set (a : Array α) (i : @& Fin a.size) (v : α) : Array α := {\n  data := a.data.set i.val v\n}\n\n@[inline] def Array.setD (a : Array α) (i : Nat) (v : α) : Array α :=\n  dite (Less i a.size) (fun h => a.set ⟨i, h⟩ v) (fun _ => a)\n\n@[extern \"lean_array_set\"]\ndef Array.set! (a : Array α) (i : @& Nat) (v : α) : Array α :=\n  Array.setD a i v\n\n-- Slower `Array.append` used in quotations.\nprotected def Array.appendCore {α : Type u}  (as : Array α) (bs : Array α) : Array α :=\n  let rec loop (i : Nat) (j : Nat) (as : Array α) : Array α :=\n    dite (Less j bs.size)\n      (fun hlt =>\n        match i with\n        | 0           => as\n        | Nat.succ i' => loop i' (hAdd j 1) (as.push (bs.get ⟨j, hlt⟩)))\n      (fun _ => as)\n  loop bs.size 0 as\n\nclass Bind (m : Type u → Type v) where\n  bind : {α β : Type u} → m α → (α → m β) → m β\n\nexport Bind (bind)\n\nclass Pure (f : Type u → Type v) where\n  pure {α : Type u} : α → f α\n\nexport Pure (pure)\n\nclass Functor (f : Type u → Type v) : Type (max (u+1) v) where\n  map      : {α β : Type u} → (α → β) → f α → f β\n  mapConst : {α β : Type u} → α → f β → f α := Function.comp map (Function.const _)\n\nclass Seq (f : Type u → Type v) : Type (max (u+1) v) where\n  seq  : {α β : Type u} → f (α → β) → f α → f β\n\nclass SeqLeft (f : Type u → Type v) : Type (max (u+1) v) where\n  seqLeft : {α β : Type u} → f α → f β → f α\n\nclass SeqRight (f : Type u → Type v) : Type (max (u+1) v) where\n  seqRight : {α β : Type u} → f α → f β → f β\n\nclass Applicative (f : Type u → Type v) extends Functor f, Pure f, Seq f, SeqLeft f, SeqRight f where\n  map      := fun x y => Seq.seq (pure x) y\n  seqLeft  := fun a b => Seq.seq (Functor.map (Function.const _) a) b\n  seqRight := fun a b => Seq.seq (Functor.map (Function.const _ id) a) b\n\nclass Monad (m : Type u → Type v) extends Applicative m, Bind m : Type (max (u+1) v) where\n  map      := fun f x => bind x (Function.comp pure f)\n  seq      := fun f x => bind f fun y => Functor.map y x\n  seqLeft  := fun x y => bind x fun a => bind y (fun _ => pure a)\n  seqRight := fun x y => bind x fun _ => y\n\ninstance {α : Type u} {m : Type u → Type v} [Monad m] : Inhabited (α → m α) where\n  default := pure\n\ninstance {α : Type u} {m : Type u → Type v} [Monad m] [Inhabited α] : Inhabited (m α) where\n  default := pure arbitrary\n\n-- A fusion of Haskell's `sequence` and `map`\ndef Array.sequenceMap {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m β) : m (Array β) :=\n  let rec loop (i : Nat) (j : Nat) (bs : Array β) : m (Array β) :=\n    dite (Less j as.size)\n      (fun hlt =>\n        match i with\n        | 0           => pure bs\n        | Nat.succ i' => Bind.bind (f (as.get ⟨j, hlt⟩)) fun b => loop i' (hAdd j 1) (bs.push b))\n      (fun _ => bs)\n  loop as.size 0 Array.empty\n\n/-- A Function for lifting a computation from an inner Monad to an outer Monad.\n    Like [MonadTrans](https://hackage.haskell.org/package/transformers-0.5.5.0/docs/Control-Monad-Trans-Class.html),\n    but `n` does not have to be a monad transformer.\n    Alternatively, an implementation of [MonadLayer](https://hackage.haskell.org/package/layers-0.1/docs/Control-Monad-Layer.html#t:MonadLayer) without `layerInvmap` (so far). -/\nclass MonadLift (m : Type u → Type v) (n : Type u → Type w) where\n  monadLift : {α : Type u} → m α → n α\n\n/-- The reflexive-transitive closure of `MonadLift`.\n    `monadLift` is used to transitively lift monadic computations such as `StateT.get` or `StateT.put s`.\n    Corresponds to [MonadLift](https://hackage.haskell.org/package/layers-0.1/docs/Control-Monad-Layer.html#t:MonadLift). -/\nclass MonadLiftT (m : Type u → Type v) (n : Type u → Type w) where\n  monadLift : {α : Type u} → m α → n α\n\nexport MonadLiftT (monadLift)\n\nabbrev liftM := @monadLift\n\ninstance (m n o) [MonadLift n o] [MonadLiftT m n] : MonadLiftT m o where\n  monadLift x := MonadLift.monadLift (m := n) (monadLift x)\n\ninstance (m) : MonadLiftT m m where\n  monadLift x := x\n\n/-- A functor in the category of monads. Can be used to lift monad-transforming functions.\n    Based on pipes' [MFunctor](https://hackage.haskell.org/package/pipes-2.4.0/docs/Control-MFunctor.html),\n    but not restricted to monad transformers.\n    Alternatively, an implementation of [MonadTransFunctor](http://duairc.netsoc.ie/layers-docs/Control-Monad-Layer.html#t:MonadTransFunctor). -/\nclass MonadFunctor (m : Type u → Type v) (n : Type u → Type w) where\n  monadMap {α : Type u} : ({β : Type u} → m β → m β) → n α → n α\n\n/-- The reflexive-transitive closure of `MonadFunctor`.\n    `monadMap` is used to transitively lift Monad morphisms -/\nclass MonadFunctorT (m : Type u → Type v) (n : Type u → Type w) where\n  monadMap {α : Type u} : ({β : Type u} → m β → m β) → n α → n α\n\nexport MonadFunctorT (monadMap)\n\ninstance (m n o) [MonadFunctor n o] [MonadFunctorT m n] : MonadFunctorT m o where\n  monadMap f := MonadFunctor.monadMap (m := n) (monadMap (m := m) f)\n\ninstance monadFunctorRefl (m) : MonadFunctorT m m where\n  monadMap f := f\n\ninductive Except (ε : Type u) (α : Type v) where\n  | error : ε → Except ε α\n  | ok    : α → Except ε α\n\nattribute [unbox] Except\n\ninstance {ε : Type u} {α : Type v} [Inhabited ε] : Inhabited (Except ε α) where\n  default := Except.error arbitrary\n\n/-- An implementation of [MonadError](https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Except.html#t:MonadError) -/\nclass MonadExceptOf (ε : Type u) (m : Type v → Type w) where\n  throw {α : Type v} : ε → m α\n  tryCatch {α : Type v} : m α → (ε → m α) → m α\n\nabbrev throwThe (ε : Type u) {m : Type v → Type w} [MonadExceptOf ε m] {α : Type v} (e : ε) : m α :=\n  MonadExceptOf.throw e\n\nabbrev tryCatchThe (ε : Type u) {m : Type v → Type w} [MonadExceptOf ε m] {α : Type v} (x : m α) (handle : ε → m α) : m α :=\n  MonadExceptOf.tryCatch x handle\n\n/-- Similar to `MonadExceptOf`, but `ε` is an outParam for convenience -/\nclass MonadExcept (ε : outParam (Type u)) (m : Type v → Type w) where\n  throw {α : Type v} : ε → m α\n  tryCatch {α : Type v} : m α → (ε → m α) → m α\n\nexport MonadExcept (throw tryCatch)\n\ninstance (ε : outParam (Type u)) (m : Type v → Type w) [MonadExceptOf ε m] : MonadExcept ε m where\n  throw    := throwThe ε\n  tryCatch := tryCatchThe ε\n\nnamespace MonadExcept\nvariable {ε : Type u} {m : Type v → Type w}\n\n@[inline] protected def orelse [MonadExcept ε m] {α : Type v} (t₁ t₂ : m α) : m α :=\n  tryCatch t₁ fun _ => t₂\n\ninstance [MonadExcept ε m] {α : Type v} : OrElse (m α) where\n  orElse := MonadExcept.orelse\n\nend MonadExcept\n\n/-- An implementation of [ReaderT](https://hackage.haskell.org/package/transformers-0.5.5.0/docs/Control-Monad-Trans-Reader.html#t:ReaderT) -/\ndef ReaderT (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=\n  ρ → m α\n\ninstance (ρ : Type u) (m : Type u → Type v) (α : Type u) [Inhabited (m α)] : Inhabited (ReaderT ρ m α) where\n  default := fun _ => arbitrary\n\n@[inline] def ReaderT.run {ρ : Type u} {m : Type u → Type v} {α : Type u} (x : ReaderT ρ m α) (r : ρ) : m α :=\n  x r\n\nnamespace ReaderT\n\nsection\nvariable {ρ : Type u} {m : Type u → Type v} {α : Type u}\n\ninstance  : MonadLift m (ReaderT ρ m) where\n  monadLift x := fun _ => x\n\ninstance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (ReaderT ρ m) where\n  throw e  := liftM (m := m) (throw e)\n  tryCatch := fun x c r => tryCatchThe ε (x r) (fun e => (c e) r)\n\nend\n\nsection\nvariable {ρ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u}\n\n@[inline] protected def read : ReaderT ρ m ρ :=\n  pure\n\n@[inline] protected def pure (a : α) : ReaderT ρ m α :=\n  fun r => pure a\n\n@[inline] protected def bind (x : ReaderT ρ m α) (f : α → ReaderT ρ m β) : ReaderT ρ m β :=\n  fun r => bind (x r) fun a => f a r\n\n@[inline] protected def map (f : α → β) (x : ReaderT ρ m α) : ReaderT ρ m β :=\n  fun r => Functor.map f (x r)\n\ninstance : Monad (ReaderT ρ m) where\n  pure := ReaderT.pure\n  bind := ReaderT.bind\n  map  := ReaderT.map\n\ninstance (ρ m) [Monad m] : MonadFunctor m (ReaderT ρ m) where\n  monadMap f x := fun ctx => f (x ctx)\n\n@[inline] protected def adapt {ρ' : Type u} [Monad m] {α : Type u} (f : ρ' → ρ) : ReaderT ρ m α → ReaderT ρ' m α :=\n  fun x r => x (f r)\n\nend\nend ReaderT\n\n/-- An implementation of [MonadReader](https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Reader-Class.html#t:MonadReader).\n    It does not contain `local` because this Function cannot be lifted using `monadLift`.\n    Instead, the `MonadReaderAdapter` class provides the more general `adaptReader` Function.\n\n    Note: This class can be seen as a simplification of the more \"principled\" definition\n    ```\n    class MonadReader (ρ : outParam (Type u)) (n : Type u → Type u) where\n      lift {α : Type u} : ({m : Type u → Type u} → [Monad m] → ReaderT ρ m α) → n α\n    ```\n    -/\nclass MonadReaderOf (ρ : Type u) (m : Type u → Type v) where\n  read : m ρ\n\n@[inline] def readThe (ρ : Type u) {m : Type u → Type v} [MonadReaderOf ρ m] : m ρ :=\n  MonadReaderOf.read\n\n/-- Similar to `MonadReaderOf`, but `ρ` is an outParam for convenience -/\nclass MonadReader (ρ : outParam (Type u)) (m : Type u → Type v) where\n  read : m ρ\n\nexport MonadReader (read)\n\ninstance (ρ : Type u) (m : Type u → Type v) [MonadReaderOf ρ m] : MonadReader ρ m where\n  read := readThe ρ\n\ninstance {ρ : Type u} {m : Type u → Type v} {n : Type u → Type w} [MonadLift m n] [MonadReaderOf ρ m] : MonadReaderOf ρ n where\n  read := liftM (m := m) read\n\ninstance {ρ : Type u} {m : Type u → Type v} [Monad m] : MonadReaderOf ρ (ReaderT ρ m) where\n  read := ReaderT.read\n\nclass MonadWithReaderOf (ρ : Type u) (m : Type u → Type v) where\n  withReader {α : Type u} : (ρ → ρ) → m α → m α\n\n@[inline] def withTheReader (ρ : Type u) {m : Type u → Type v} [MonadWithReaderOf ρ m] {α : Type u} (f : ρ → ρ) (x : m α) : m α :=\n  MonadWithReaderOf.withReader f x\n\nclass MonadWithReader (ρ : outParam (Type u)) (m : Type u → Type v) where\n  withReader {α : Type u} : (ρ → ρ) → m α → m α\n\nexport MonadWithReader (withReader)\n\ninstance (ρ : Type u) (m : Type u → Type v) [MonadWithReaderOf ρ m] : MonadWithReader ρ m where\n  withReader := withTheReader ρ\n\ninstance {ρ : Type u} {m : Type u → Type v} {n : Type u → Type v} [MonadFunctor m n] [MonadWithReaderOf ρ m] : MonadWithReaderOf ρ n where\n  withReader f := monadMap (m := m) (withTheReader ρ f)\n\ninstance {ρ : Type u} {m : Type u → Type v} [Monad m] : MonadWithReaderOf ρ (ReaderT ρ m) where\n  withReader f x := fun ctx => x (f ctx)\n\n/-- An implementation of [MonadState](https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-State-Class.html).\n    In contrast to the Haskell implementation, we use overlapping instances to derive instances\n    automatically from `monadLift`. -/\nclass MonadStateOf (σ : Type u) (m : Type u → Type v) where\n  /- Obtain the top-most State of a Monad stack. -/\n  get : m σ\n  /- Set the top-most State of a Monad stack. -/\n  set : σ → m PUnit\n  /- Map the top-most State of a Monad stack.\n\n     Note: `modifyGet f` may be preferable to `do s <- get; let (a, s) := f s; put s; pure a`\n     because the latter does not use the State linearly (without sufficient inlining). -/\n  modifyGet {α : Type u} : (σ → Prod α σ) → m α\n\nexport MonadStateOf (set)\n\nabbrev getThe (σ : Type u) {m : Type u → Type v} [MonadStateOf σ m] : m σ :=\n  MonadStateOf.get\n\n@[inline] abbrev modifyThe (σ : Type u) {m : Type u → Type v} [MonadStateOf σ m] (f : σ → σ) : m PUnit :=\n  MonadStateOf.modifyGet fun s => (PUnit.unit, f s)\n\n@[inline] abbrev modifyGetThe {α : Type u} (σ : Type u) {m : Type u → Type v} [MonadStateOf σ m] (f : σ → Prod α σ) : m α :=\n  MonadStateOf.modifyGet f\n\n/-- Similar to `MonadStateOf`, but `σ` is an outParam for convenience -/\nclass MonadState (σ : outParam (Type u)) (m : Type u → Type v) where\n  get : m σ\n  set : σ → m PUnit\n  modifyGet {α : Type u} : (σ → Prod α σ) → m α\n\nexport MonadState (get modifyGet)\n\ninstance (σ : Type u) (m : Type u → Type v) [MonadStateOf σ m] : MonadState σ m where\n  set       := MonadStateOf.set\n  get       := getThe σ\n  modifyGet := fun f => MonadStateOf.modifyGet f\n\n@[inline] def modify {σ : Type u} {m : Type u → Type v} [MonadState σ m] (f : σ → σ) : m PUnit :=\n  modifyGet fun s => (PUnit.unit, f s)\n\n@[inline] def getModify {σ : Type u} {m : Type u → Type v} [MonadState σ m] [Monad m] (f : σ → σ) : m σ :=\n  modifyGet fun s => (s, f s)\n\n-- NOTE: The Ordering of the following two instances determines that the top-most `StateT` Monad layer\n-- will be picked first\ninstance {σ : Type u} {m : Type u → Type v} {n : Type u → Type w} [MonadLift m n] [MonadStateOf σ m] : MonadStateOf σ n where\n  get       := liftM (m := m) MonadStateOf.get\n  set       := fun s => liftM (m := m) (MonadStateOf.set s)\n  modifyGet := fun f => monadLift (m := m) (MonadState.modifyGet f)\n\nnamespace EStateM\n\ninductive Result (ε σ α : Type u) where\n  | ok    : α → σ → Result ε σ α\n  | error : ε → σ → Result ε σ α\n\nvariable {ε σ α : Type u}\n\ninstance [Inhabited ε] [Inhabited σ] : Inhabited (Result ε σ α) where\n  default := Result.error arbitrary arbitrary\n\nend EStateM\n\nopen EStateM (Result) in\ndef EStateM (ε σ α : Type u) := σ → Result ε σ α\n\nnamespace EStateM\n\nvariable {ε σ α β : Type u}\n\ninstance [Inhabited ε] : Inhabited (EStateM ε σ α) where\n  default := fun s => Result.error arbitrary s\n\n@[inline] protected def pure (a : α) : EStateM ε σ α := fun s =>\n  Result.ok a s\n\n@[inline] protected def set (s : σ) : EStateM ε σ PUnit := fun _ =>\n  Result.ok ⟨⟩ s\n\n@[inline] protected def get : EStateM ε σ σ := fun s =>\n  Result.ok s s\n\n@[inline] protected def modifyGet (f : σ → Prod α σ) : EStateM ε σ α := fun s =>\n  match f s with\n  | (a, s) => Result.ok a s\n\n@[inline] protected def throw (e : ε) : EStateM ε σ α := fun s =>\n  Result.error e s\n\n/-- Auxiliary instance for saving/restoring the \"backtrackable\" part of the state. -/\nclass Backtrackable (δ : outParam (Type u)) (σ : Type u) where\n  save    : σ → δ\n  restore : σ → δ → σ\n\n@[inline] protected def tryCatch {δ} [Backtrackable δ σ] {α} (x : EStateM ε σ α) (handle : ε → EStateM ε σ α) : EStateM ε σ α := fun s =>\n  let d := Backtrackable.save s\n  match x s with\n  | Result.error e s => handle e (Backtrackable.restore s d)\n  | ok               => ok\n\n@[inline] protected def orElse {δ} [Backtrackable δ σ] (x₁ x₂ : EStateM ε σ α) : EStateM ε σ α := fun s =>\n  let d := Backtrackable.save s;\n  match x₁ s with\n  | Result.error _ s => x₂ (Backtrackable.restore s d)\n  | ok               => ok\n\n@[inline] def adaptExcept {ε' : Type u} (f : ε → ε') (x : EStateM ε σ α) : EStateM ε' σ α := fun s =>\n  match x s with\n  | Result.error e s => Result.error (f e) s\n  | Result.ok a s    => Result.ok a s\n\n@[inline] protected def bind (x : EStateM ε σ α) (f : α → EStateM ε σ β) : EStateM ε σ β := fun s =>\n  match x s with\n  | Result.ok a s    => f a s\n  | Result.error e s => Result.error e s\n\n@[inline] protected def map (f : α → β) (x : EStateM ε σ α) : EStateM ε σ β := fun s =>\n  match x s with\n  | Result.ok a s    => Result.ok (f a) s\n  | Result.error e s => Result.error e s\n\n@[inline] protected def seqRight (x : EStateM ε σ α) (y : EStateM ε σ β) : EStateM ε σ β := fun s =>\n  match x s with\n  | Result.ok _ s    => y s\n  | Result.error e s => Result.error e s\n\ninstance : Monad (EStateM ε σ) where\n  bind     := EStateM.bind\n  pure     := EStateM.pure\n  map      := EStateM.map\n  seqRight := EStateM.seqRight\n\ninstance {δ} [Backtrackable δ σ] : OrElse (EStateM ε σ α) where\n  orElse := EStateM.orElse\n\ninstance : MonadStateOf σ (EStateM ε σ) where\n  set       := EStateM.set\n  get       := EStateM.get\n  modifyGet := EStateM.modifyGet\n\ninstance {δ} [Backtrackable δ σ] : MonadExceptOf ε (EStateM ε σ) where\n  throw    := EStateM.throw\n  tryCatch := EStateM.tryCatch\n\n@[inline] def run (x : EStateM ε σ α) (s : σ) : Result ε σ α :=\n  x s\n\n@[inline] def run' (x : EStateM ε σ α) (s : σ) : Option α :=\n  match run x s with\n  | Result.ok v _    => some v\n  | Result.error _ _ => none\n\n@[inline] def dummySave : σ → PUnit := fun _ => ⟨⟩\n\n@[inline] def dummyRestore : σ → PUnit → σ := fun s _ => s\n\n/- Dummy default instance -/\ninstance nonBacktrackable : Backtrackable PUnit σ where\n  save    := dummySave\n  restore := dummyRestore\n\nend EStateM\n\nclass Hashable (α : Type u) where\n  hash : α → USize\n\nexport Hashable (hash)\n\n@[extern \"lean_usize_mix_hash\"]\nconstant mixHash (u₁ u₂ : USize) : USize\n\n@[extern \"lean_string_hash\"]\nprotected constant String.hash (s : @& String) : USize\n\ninstance : Hashable String where\n  hash := String.hash\n\nnamespace Lean\n\n/- Hierarchical names -/\ninductive Name where\n  | anonymous : Name\n  | str : Name → String → USize → Name\n  | num : Name → Nat → USize → Name\n\ninstance : Inhabited Name where\n  default := Name.anonymous\n\nprotected def Name.hash : Name → USize\n  | Name.anonymous => USize.ofNat32 1723 (by decide)\n  | Name.str p s h => h\n  | Name.num p v h => h\n\ninstance : Hashable Name where\n  hash := Name.hash\n\nnamespace Name\n\n@[export lean_name_mk_string]\ndef mkStr (p : Name) (s : String) : Name :=\n  Name.str p s (mixHash (hash p) (hash s))\n\n@[export lean_name_mk_numeral]\ndef mkNum (p : Name) (v : Nat) : Name :=\n  Name.num p v (mixHash (hash p) (dite (Less v USize.size) (fun h => USize.ofNatCore v h) (fun _ => USize.ofNat32 17 (by decide))))\n\ndef mkSimple (s : String) : Name :=\n  mkStr Name.anonymous s\n\n@[extern \"lean_name_eq\"]\nprotected def beq : (@& Name) → (@& Name) → Bool\n  | anonymous,   anonymous   => true\n  | str p₁ s₁ _, str p₂ s₂ _ => and (BEq.beq s₁ s₂) (Name.beq p₁ p₂)\n  | num p₁ n₁ _, num p₂ n₂ _ => and (BEq.beq n₁ n₂) (Name.beq p₁ p₂)\n  | _,           _           => false\n\ninstance : BEq Name where\n  beq := Name.beq\n\nprotected def append : Name → Name → Name\n  | n, anonymous => n\n  | n, str p s _ => Name.mkStr (Name.append n p) s\n  | n, num p d _ => Name.mkNum (Name.append n p) d\n\ninstance : Append Name where\n  append := Name.append\n\nend Name\n\n/- Syntax -/\n\n/-- Source information of tokens. -/\ninductive SourceInfo where\n  /-\n    Token from original input with whitespace and position information.\n    `leading` will be inferred after parsing by `Syntax.updateLeading`. During parsing,\n    it is not at all clear what the preceding token was, especially with backtracking. -/\n  | original (leading : Substring) (pos : String.Pos) (trailing : Substring)\n  /-\n    Synthesized token (e.g. from a quotation) annotated with a span from the original source.\n    In the delaborator, we \"misuse\" this constructor to store synthetic positions identifying\n    subterms. -/\n  | synthetic (pos : String.Pos) (endPos : String.Pos)\n  /- Synthesized token without position information. -/\n  | protected none\n\ninstance : Inhabited SourceInfo := ⟨SourceInfo.none⟩\n\nnamespace SourceInfo\n\ndef getPos? (info : SourceInfo) (originalOnly := false) : Option String.Pos :=\n  match info, originalOnly with\n  | original (pos := pos) ..,  _     => some pos\n  | synthetic (pos := pos) .., false => some pos\n  | _,                         _     => none\n\nend SourceInfo\n\nabbrev SyntaxNodeKind := Name\n\n/- Syntax AST -/\n\ninductive Syntax where\n  | missing : Syntax\n  | node   (kind : SyntaxNodeKind) (args : Array Syntax) : Syntax\n  | atom   (info : SourceInfo) (val : String) : Syntax\n  | ident  (info : SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List (Prod Name (List String))) : Syntax\n\ninstance : Inhabited Syntax where\n  default := Syntax.missing\n\n/- Builtin kinds -/\ndef choiceKind : SyntaxNodeKind := `choice\ndef nullKind : SyntaxNodeKind := `null\ndef identKind : SyntaxNodeKind := `ident\ndef strLitKind : SyntaxNodeKind := `strLit\ndef charLitKind : SyntaxNodeKind := `charLit\ndef numLitKind : SyntaxNodeKind := `numLit\ndef scientificLitKind : SyntaxNodeKind := `scientificLit\ndef nameLitKind : SyntaxNodeKind := `nameLit\ndef fieldIdxKind : SyntaxNodeKind := `fieldIdx\ndef interpolatedStrLitKind : SyntaxNodeKind := `interpolatedStrLitKind\ndef interpolatedStrKind : SyntaxNodeKind := `interpolatedStrKind\n\nnamespace Syntax\n\ndef getKind (stx : Syntax) : SyntaxNodeKind :=\n  match stx with\n  | Syntax.node k args   => k\n  -- We use these \"pseudo kinds\" for antiquotation kinds.\n  -- For example, an antiquotation `$id:ident` (using Lean.Parser.Term.ident)\n  -- is compiled to ``if stx.isOfKind `ident ...``\n  | Syntax.missing       => `missing\n  | Syntax.atom _ v      => Name.mkSimple v\n  | Syntax.ident _ _ _ _ => identKind\n\ndef setKind (stx : Syntax) (k : SyntaxNodeKind) : Syntax :=\n  match stx with\n  | Syntax.node _ args => Syntax.node k args\n  | _                  => stx\n\ndef isOfKind (stx : Syntax) (k : SyntaxNodeKind) : Bool :=\n  beq stx.getKind k\n\ndef getArg (stx : Syntax) (i : Nat) : Syntax :=\n  match stx with\n  | Syntax.node _ args => args.getD i Syntax.missing\n  | _                  => Syntax.missing\n\n-- Add `stx[i]` as sugar for `stx.getArg i`\n@[inline] def getOp (self : Syntax) (idx : Nat) : Syntax :=\n  self.getArg idx\n\ndef getArgs (stx : Syntax) : Array Syntax :=\n  match stx with\n  | Syntax.node _ args => args\n  | _                  => Array.empty\n\ndef getNumArgs (stx : Syntax) : Nat :=\n  match stx with\n  | Syntax.node _ args => args.size\n  | _                  => 0\n\ndef setArgs (stx : Syntax) (args : Array Syntax) : Syntax :=\n  match stx with\n  | node k _ => node k args\n  | stx      => stx\n\ndef setArg (stx : Syntax) (i : Nat) (arg : Syntax) : Syntax :=\n  match stx with\n  | node k args => node k (args.setD i arg)\n  | stx         => stx\n\n/-- Retrieve the left-most leaf's info in the Syntax tree. -/\npartial def getHeadInfo? : Syntax → Option SourceInfo\n  | atom info _      => some info\n  | ident info _ _ _ => some info\n  | node _ args      =>\n    let rec loop (i : Nat) : Option SourceInfo :=\n      match decide (Less i args.size) with\n      | true => match getHeadInfo? (args.get! i) with\n         | some info => some info\n         | none      => loop (hAdd i 1)\n      | false => none\n    loop 0\n  | _                => none\n\n/-- Retrieve the left-most leaf's info in the Syntax tree, or `none` if there is no token. -/\npartial def getHeadInfo (stx : Syntax) : SourceInfo :=\n  match stx.getHeadInfo? with\n  | some info => info\n  | none      => SourceInfo.none\n\ndef getPos? (stx : Syntax) (originalOnly := false) : Option String.Pos :=\n  stx.getHeadInfo.getPos? originalOnly\n\npartial def getTailPos? (stx : Syntax) (originalOnly := false) : Option String.Pos :=\n  match stx, originalOnly with\n  | atom (SourceInfo.original (pos := pos) ..) val,    _      => some (pos.add val.bsize)\n  | atom (SourceInfo.synthetic (endPos := pos) ..) _,  false  => some pos\n  | ident (SourceInfo.original (pos := pos) ..) val .., _     => some (pos.add val.bsize)\n  | ident (SourceInfo.synthetic (endPos := pos) ..) .., false => some pos\n  | node _ args,                                        _     =>\n    let rec loop (i : Nat) : Option String.Pos :=\n      match decide (Less i args.size) with\n      | true => match getTailPos? (args.get! ((args.size.sub i).sub 1)) with\n         | some info => some info\n         | none      => loop (hAdd i 1)\n      | false => none\n    loop 0\n  | _, _ => none\n\n/--\n  An array of syntax elements interspersed with separators. Can be coerced to/from `Array Syntax` to automatically\n  remove/insert the separators. -/\nstructure SepArray (sep : String) where\n  elemsAndSeps : Array Syntax\n\nend Syntax\n\ndef SourceInfo.fromRef (ref : Syntax) : SourceInfo :=\n  match ref.getPos?, ref.getTailPos? with\n  | some pos, some tailPos => SourceInfo.synthetic pos tailPos\n  | _,        _            => SourceInfo.none\n\ndef mkAtomFrom (src : Syntax) (val : String) : Syntax :=\n  Syntax.atom src.getHeadInfo val\n\n/- Parser descriptions -/\n\ninductive ParserDescr where\n  | const  (name : Name)\n  | unary  (name : Name) (p : ParserDescr)\n  | binary (name : Name) (p₁ p₂ : ParserDescr)\n  | node (kind : SyntaxNodeKind) (prec : Nat) (p : ParserDescr)\n  | trailingNode (kind : SyntaxNodeKind) (prec : Nat) (p : ParserDescr)\n  | symbol (val : String)\n  | nonReservedSymbol (val : String) (includeIdent : Bool)\n  | cat (catName : Name) (rbp : Nat)\n  | parser (declName : Name)\n  | nodeWithAntiquot (name : String) (kind : SyntaxNodeKind) (p : ParserDescr)\n  | sepBy  (p : ParserDescr) (sep : String) (psep : ParserDescr) (allowTrailingSep : Bool := false)\n  | sepBy1 (p : ParserDescr) (sep : String) (psep : ParserDescr) (allowTrailingSep : Bool := false)\n\ninstance : Inhabited ParserDescr where\n  default := ParserDescr.symbol \"\"\n\nabbrev TrailingParserDescr := ParserDescr\n\n/-\nRuntime support for making quotation terms auto-hygienic, by mangling identifiers\nintroduced by them with a \"macro scope\" supplied by the context. Details to appear in a\npaper soon.\n-/\n\nabbrev MacroScope := Nat\n/-- Macro scope used internally. It is not available for our frontend. -/\ndef reservedMacroScope := 0\n/-- First macro scope available for our frontend -/\ndef firstFrontendMacroScope := hAdd reservedMacroScope 1\n\nclass MonadRef (m : Type → Type) where\n  getRef      : m Syntax\n  withRef {α} : Syntax → m α → m α\n\nexport MonadRef (getRef)\n\ninstance (m n : Type → Type) [MonadLift m n] [MonadFunctor m n] [MonadRef m] : MonadRef n where\n  getRef  := liftM (getRef : m _)\n  withRef := fun ref x => monadMap (m := m) (MonadRef.withRef ref) x\n\ndef replaceRef (ref : Syntax) (oldRef : Syntax) : Syntax :=\n  match ref.getPos? with\n  | some _ => ref\n  | _      => oldRef\n\n@[inline] def withRef {m : Type → Type} [Monad m] [MonadRef m] {α} (ref : Syntax) (x : m α) : m α :=\n  bind getRef fun oldRef =>\n  let ref := replaceRef ref oldRef\n  MonadRef.withRef ref x\n\n/-- A monad that supports syntax quotations. Syntax quotations (in term\n    position) are monadic values that when executed retrieve the current \"macro\n    scope\" from the monad and apply it to every identifier they introduce\n    (independent of whether this identifier turns out to be a reference to an\n    existing declaration, or an actually fresh binding during further\n    elaboration). We also apply the position of the result of `getRef` to each\n    introduced symbol, which results in better error positions than not applying\n    any position. -/\nclass MonadQuotation (m : Type → Type) extends MonadRef m where\n  -- Get the fresh scope of the current macro invocation\n  getCurrMacroScope : m MacroScope\n  getMainModule     : m Name\n  /- Execute action in a new macro invocation context. This transformer should be\n     used at all places that morally qualify as the beginning of a \"macro call\",\n     e.g. `elabCommand` and `elabTerm` in the case of the elaborator. However, it\n     can also be used internally inside a \"macro\" if identifiers introduced by\n     e.g. different recursive calls should be independent and not collide. While\n     returning an intermediate syntax tree that will recursively be expanded by\n     the elaborator can be used for the same effect, doing direct recursion inside\n     the macro guarded by this transformer is often easier because one is not\n     restricted to passing a single syntax tree. Modelling this helper as a\n     transformer and not just a monadic action ensures that the current macro\n     scope before the recursive call is restored after it, as expected. -/\n  withFreshMacroScope {α : Type} : m α → m α\n\nexport MonadQuotation (getCurrMacroScope getMainModule withFreshMacroScope)\n\ndef MonadRef.mkInfoFromRefPos [Monad m] [MonadRef m] : m SourceInfo := do\n  SourceInfo.fromRef (← getRef)\n\ninstance {m n : Type → Type} [MonadFunctor m n] [MonadLift m n] [MonadQuotation m] : MonadQuotation n where\n  getCurrMacroScope   := liftM (m := m) getCurrMacroScope\n  getMainModule       := liftM (m := m) getMainModule\n  withFreshMacroScope := monadMap (m := m) withFreshMacroScope\n\n/-\nWe represent a name with macro scopes as\n```\n<actual name>._@.(<module_name>.<scopes>)*.<module_name>._hyg.<scopes>\n```\nExample: suppose the module name is `Init.Data.List.Basic`, and name is `foo.bla`, and macroscopes [2, 5]\n```\nfoo.bla._@.Init.Data.List.Basic._hyg.2.5\n```\n\nWe may have to combine scopes from different files/modules.\nThe main modules being processed is always the right most one.\nThis situation may happen when we execute a macro generated in\nan imported file in the current file.\n```\nfoo.bla._@.Init.Data.List.Basic.2.1.Init.Lean.Expr_hyg.4\n```\n\nThe delimiter `_hyg` is used just to improve the `hasMacroScopes` performance.\n-/\n\ndef Name.hasMacroScopes : Name → Bool\n  | str _ s _   => beq s \"_hyg\"\n  | num p _   _ => hasMacroScopes p\n  | _           => false\n\nprivate def eraseMacroScopesAux : Name → Name\n  | Name.str p s _   => match beq s \"_@\" with\n    | true  => p\n    | false => eraseMacroScopesAux p\n  | Name.num p _ _   => eraseMacroScopesAux p\n  | Name.anonymous   => Name.anonymous\n\n@[export lean_erase_macro_scopes]\ndef Name.eraseMacroScopes (n : Name) : Name :=\n  match n.hasMacroScopes with\n  | true  => eraseMacroScopesAux n\n  | false => n\n\nprivate def simpMacroScopesAux : Name → Name\n  | Name.num p i _ => Name.mkNum (simpMacroScopesAux p) i\n  | n              => eraseMacroScopesAux n\n\n/- Helper function we use to create binder names that do not need to be unique. -/\n@[export lean_simp_macro_scopes]\ndef Name.simpMacroScopes (n : Name) : Name :=\n  match n.hasMacroScopes with\n  | true  => simpMacroScopesAux n\n  | false => n\n\nstructure MacroScopesView where\n  name       : Name\n  imported   : Name\n  mainModule : Name\n  scopes     : List MacroScope\n\ninstance : Inhabited MacroScopesView where\n  default := ⟨arbitrary, arbitrary, arbitrary, arbitrary⟩\n\ndef MacroScopesView.review (view : MacroScopesView) : Name :=\n  match view.scopes with\n  | List.nil      => view.name\n  | List.cons _ _ =>\n    let base := (Name.mkStr (hAppend (hAppend (Name.mkStr view.name \"_@\") view.imported) view.mainModule) \"_hyg\")\n    view.scopes.foldl Name.mkNum base\n\nprivate def assembleParts : List Name → Name → Name\n  | List.nil,                      acc => acc\n  | List.cons (Name.str _ s _) ps, acc => assembleParts ps (Name.mkStr acc s)\n  | List.cons (Name.num _ n _) ps, acc => assembleParts ps (Name.mkNum acc n)\n  | _,                             acc => panic \"Error: unreachable @ assembleParts\"\n\nprivate def extractImported (scps : List MacroScope) (mainModule : Name) : Name → List Name → MacroScopesView\n  | n@(Name.str p str _), parts =>\n    match beq str \"_@\" with\n    | true  => { name := p, mainModule := mainModule, imported := assembleParts parts Name.anonymous, scopes := scps }\n    | false => extractImported scps mainModule p (List.cons n parts)\n  | n@(Name.num p str _), parts => extractImported scps mainModule p (List.cons n parts)\n  | _,                    _     => panic \"Error: unreachable @ extractImported\"\n\nprivate def extractMainModule (scps : List MacroScope) : Name → List Name → MacroScopesView\n  | n@(Name.str p str _), parts =>\n    match beq str \"_@\" with\n    | true  => { name := p, mainModule := assembleParts parts Name.anonymous, imported := Name.anonymous, scopes := scps }\n    | false => extractMainModule scps p (List.cons n parts)\n  | n@(Name.num p num _), acc => extractImported scps (assembleParts acc Name.anonymous) n List.nil\n  | _,                    _   => panic \"Error: unreachable @ extractMainModule\"\n\nprivate def extractMacroScopesAux : Name → List MacroScope → MacroScopesView\n  | Name.num p scp _, acc => extractMacroScopesAux p (List.cons scp acc)\n  | Name.str p str _, acc => extractMainModule acc p List.nil -- str must be \"_hyg\"\n  | _,                _   => panic \"Error: unreachable @ extractMacroScopesAux\"\n\n/--\n  Revert all `addMacroScope` calls. `v = extractMacroScopes n → n = v.review`.\n  This operation is useful for analyzing/transforming the original identifiers, then adding back\n  the scopes (via `MacroScopesView.review`). -/\ndef extractMacroScopes (n : Name) : MacroScopesView :=\n  match n.hasMacroScopes with\n  | true  => extractMacroScopesAux n List.nil\n  | false => { name := n, scopes := List.nil, imported := Name.anonymous, mainModule := Name.anonymous }\n\ndef addMacroScope (mainModule : Name) (n : Name) (scp : MacroScope) : Name :=\n  match n.hasMacroScopes with\n  | true =>\n    let view := extractMacroScopes n\n    match beq view.mainModule mainModule with\n    | true  => Name.mkNum n scp\n    | false =>\n      { view with\n        imported   := view.scopes.foldl Name.mkNum (hAppend view.imported view.mainModule),\n        mainModule := mainModule,\n        scopes     := List.cons scp List.nil\n      }.review\n  | false =>\n    Name.mkNum (Name.mkStr (hAppend (Name.mkStr n \"_@\") mainModule) \"_hyg\") scp\n\n@[inline] def MonadQuotation.addMacroScope {m : Type → Type} [MonadQuotation m] [Monad m] (n : Name) : m Name :=\n  bind getMainModule     fun mainModule =>\n  bind getCurrMacroScope fun scp =>\n  pure (Lean.addMacroScope mainModule n scp)\n\ndef defaultMaxRecDepth := 512\n\ndef maxRecDepthErrorMessage : String :=\n  \"maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)\"\n\nnamespace Macro\n\n/- References -/\nconstant MacroEnvPointed : PointedType.{0}\n\ndef MacroEnv : Type := MacroEnvPointed.type\ninstance : Inhabited MacroEnv where\n  default := MacroEnvPointed.val\n\nstructure Context where\n  macroEnv       : MacroEnv\n  mainModule     : Name\n  currMacroScope : MacroScope\n  currRecDepth   : Nat := 0\n  maxRecDepth    : Nat := defaultMaxRecDepth\n  ref            : Syntax\n\ninductive Exception where\n  | error             : Syntax → String → Exception\n  | unsupportedSyntax : Exception\n\nend Macro\n\nabbrev MacroM := ReaderT Macro.Context (EStateM Macro.Exception MacroScope)\n\nabbrev Macro := Syntax → MacroM Syntax\n\nnamespace Macro\n\ninstance : MonadRef MacroM where\n  getRef     := bind read fun ctx => pure ctx.ref\n  withRef    := fun ref x => withReader (fun ctx => { ctx with ref := ref }) x\n\ndef addMacroScope (n : Name) : MacroM Name :=\n  bind read fun ctx =>\n  pure (Lean.addMacroScope ctx.mainModule n ctx.currMacroScope)\n\ndef throwUnsupported {α} : MacroM α :=\n  throw Exception.unsupportedSyntax\n\ndef throwError {α} (msg : String) : MacroM α :=\n  bind getRef fun ref =>\n  throw (Exception.error ref msg)\n\ndef throwErrorAt {α} (ref : Syntax) (msg : String) : MacroM α :=\n  withRef ref (throwError msg)\n\n@[inline] protected def withFreshMacroScope {α} (x : MacroM α) : MacroM α :=\n  bind (modifyGet (fun s => (s, hAdd s 1))) fun fresh =>\n  withReader (fun ctx => { ctx with currMacroScope := fresh }) x\n\n@[inline] def withIncRecDepth {α} (ref : Syntax) (x : MacroM α) : MacroM α :=\n  bind read fun ctx =>\n  match beq ctx.currRecDepth ctx.maxRecDepth with\n  | true  => throw (Exception.error ref maxRecDepthErrorMessage)\n  | false => withReader (fun ctx => { ctx with currRecDepth := hAdd ctx.currRecDepth 1 }) x\n\ninstance : MonadQuotation MacroM where\n  getCurrMacroScope   := fun ctx => pure ctx.currMacroScope\n  getMainModule       := fun ctx => pure ctx.mainModule\n  withFreshMacroScope := Macro.withFreshMacroScope\n\nunsafe def mkMacroEnvImp (expandMacro? : Syntax → MacroM (Option Syntax)) : MacroEnv :=\n  unsafeCast expandMacro?\n\n@[implementedBy mkMacroEnvImp]\nconstant mkMacroEnv (expandMacro? : Syntax → MacroM (Option Syntax)) : MacroEnv\n\ndef expandMacroNotAvailable? (stx : Syntax) : MacroM (Option Syntax) :=\n  throwErrorAt stx \"expandMacro has not been set\"\n\ndef mkMacroEnvSimple : MacroEnv :=\n  mkMacroEnv expandMacroNotAvailable?\n\nunsafe def expandMacro?Imp (stx : Syntax) : MacroM (Option Syntax) :=\n  bind read fun ctx =>\n  let f : Syntax → MacroM (Option Syntax) := unsafeCast (ctx.macroEnv)\n  f stx\n\n/-- `expandMacro? stx` return `some stxNew` if `stx` is a macro, and `stxNew` is its expansion. -/\n@[implementedBy expandMacro?Imp] constant expandMacro? : Syntax → MacroM (Option Syntax)\n\nend Macro\n\nexport Macro (expandMacro?)\n\nnamespace PrettyPrinter\n\nabbrev UnexpandM := EStateM Unit Unit\n\n/--\n  Function that tries to reverse macro expansions as a post-processing step of delaboration.\n  While less general than an arbitrary delaborator, it can be declared without importing `Lean`.\n  Used by the `[appUnexpander]` attribute. -/\n-- a `kindUnexpander` could reasonably be added later\nabbrev Unexpander := Syntax → UnexpandM Syntax\n\n-- unexpanders should not need to introduce new names\ninstance : MonadQuotation UnexpandM where\n  getRef              := pure Syntax.missing\n  withRef             := fun _ => id\n  getCurrMacroScope   := pure 0\n  getMainModule       := pure `_fakeMod\n  withFreshMacroScope := id\n\nend PrettyPrinter\n\nend Lean\n"}}}