Init.NotationExtra

Lean.expandBrackedBinders combinatorDeclName bracketedExplicitBinders body = do let a ← Lean.getRef let combinator : Lean.Syntax := Lean.mkIdentFrom a combinatorDeclName Lean.expandBrackedBindersAux combinator #[bracketedExplicitBinders] body

source

def Lean.unifConstraint :

Lean.ParserDescr

Equations

Lean.unifConstraint = Lean.ParserDescr.nodeWithAntiquot "unifConstraint" `Lean.unifConstraint (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.cat `term 0) (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.symbol " =?= ") (Lean.ParserDescr.symbol " ≟ "))) (Lean.ParserDescr.cat `term 0))

source

def Lean.unifConstraintElem :

Lean.ParserDescr

Equations

Lean.unifConstraintElem = Lean.ParserDescr.nodeWithAntiquot "unifConstraintElem" `Lean.unifConstraintElem (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `colGe) Lean.unifConstraint) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.symbol ", ")))

source

def Lean.«command_Unif_hint___Where_|-⊢_» :

Lean.ParserDescr

Equations

Lean.«command_Unif_hint___Where_|-⊢_» = Lean.ParserDescr.node `Lean.«command_Unif_hint___Where_|-⊢_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `attrKind) (Lean.ParserDescr.symbol "unif_hint ")) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.const `ident))) (Lean.ParserDescr.unary `many (Lean.ParserDescr.const `bracketedBinder))) (Lean.ParserDescr.symbol " where ")) (Lean.ParserDescr.unary `withPosition (Lean.ParserDescr.unary `many Lean.unifConstraintElem))) (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.symbol "|-") (Lean.ParserDescr.symbol "⊢ "))) Lean.unifConstraint)

source

def «term∃_,_» :

Lean.ParserDescr

Equations

«term∃_,_» = Lean.ParserDescr.node `«term∃_,_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∃ ") Lean.explicitBinders) (Lean.ParserDescr.symbol ", ")) (Lean.ParserDescr.cat `term 0))

source

def «termExists_,_» :

Lean.ParserDescr

Equations

«termExists_,_» = Lean.ParserDescr.node `«termExists_,_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "exists") Lean.explicitBinders) (Lean.ParserDescr.symbol ", ")) (Lean.ParserDescr.cat `term 0))

source

def «termΣ_,_» :

Lean.ParserDescr

Equations

«termΣ_,_» = Lean.ParserDescr.node `«termΣ_,_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "Σ") Lean.explicitBinders) (Lean.ParserDescr.symbol ", ")) (Lean.ParserDescr.cat `term 0))

source

def «termΣ'_,_» :

Lean.ParserDescr

Equations

«termΣ'_,_» = Lean.ParserDescr.node `«termΣ'_,_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "Σ'") Lean.explicitBinders) (Lean.ParserDescr.symbol ", ")) (Lean.ParserDescr.cat `term 0))

source

def «term_×__1» :

Lean.ParserDescr

Equations

«term_×__1» = Lean.ParserDescr.node `«term_×__1» 35 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen Lean.bracketedExplicitBinders (Lean.ParserDescr.symbol " × ")) (Lean.ParserDescr.cat `term 35))

source

def «term_×'_» :

Lean.ParserDescr

Equations

«term_×'_» = Lean.ParserDescr.node `«term_×'_» 35 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen Lean.bracketedExplicitBinders (Lean.ParserDescr.symbol " ×' ")) (Lean.ParserDescr.cat `term 35))

source

def calcStep :

Lean.ParserDescr

Equations

calcStep = Lean.ParserDescr.nodeWithAntiquot "calcStep" `calcStep (Lean.ParserDescr.unary `ppIndent (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `colGe) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol " := ")) (Lean.ParserDescr.unary `withPosition (Lean.ParserDescr.cat `term 0))))

source

def calc :

Lean.ParserDescr

Equations

calc = Lean.ParserDescr.node `calc 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "calc") (Lean.ParserDescr.const `ppLine)) (Lean.ParserDescr.unary `withPosition (Lean.ParserDescr.unary `many1 (Lean.ParserDescr.binary `andthen calcStep (Lean.ParserDescr.const `ppLine)))))

source

def tacticCalc_ :

Lean.ParserDescr

Equations

tacticCalc_ = Lean.ParserDescr.node `tacticCalc_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "calc " false) (Lean.ParserDescr.unary `withPosition (Lean.ParserDescr.unary `many1 calcStep)))

source

def unexpandUnit :

Lean.PrettyPrinter.Unexpander

Equations

unexpandUnit _fun_discr = let discr := _fun_discr; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ")"])

source

def unexpandListNil :

Lean.PrettyPrinter.Unexpander

Equations

unexpandListNil _fun_discr = let discr := _fun_discr; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `«term[_]» #[Lean.Syntax.atom info "[", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "]"])

source

def unexpandListCons :

Lean.PrettyPrinter.Unexpander

Equations

unexpandListCons _fun_discr = let discr := _fun_discr; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.app = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_2 2 = true then let discr := Lean.Syntax.getArg discr_2 0; let discr_3 := Lean.Syntax.getArg discr_2 1; if Lean.Syntax.isOfKind discr_3 `«term[_]» = true then let discr_4 := Lean.Syntax.getArg discr_3 0; let discr_5 := Lean.Syntax.getArg discr_3 1; if Lean.Syntax.matchesNull discr_5 0 = true then let discr_6 := Lean.Syntax.getArg discr_3 2; let x := discr; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `«term[_]» #[Lean.Syntax.atom info "[", Lean.Syntax.node Lean.SourceInfo.none `null #[x], Lean.Syntax.atom info "]"]) else let discr_6 := Lean.Syntax.getArg discr_3 1; let discr_7 := Lean.Syntax.getArg discr_3 2; let xs := { elemsAndSeps := Lean.Syntax.getArgs discr_6 }; let x := discr; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `«term[_]» #[Lean.Syntax.atom info "[", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[x, Lean.Syntax.atom info ","] xs.elemsAndSeps), Lean.Syntax.atom info "]"]) else let discr := Lean.Syntax.getArg discr_2 1; throw () else let discr := Lean.Syntax.getArg discr 1; throw () else let discr := _fun_discr; throw ()

source

def unexpandListToArray :

Lean.PrettyPrinter.Unexpander

Equations

unexpandListToArray _fun_discr = let discr := _fun_discr; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.app = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_2 1 = true then let discr := Lean.Syntax.getArg discr_2 0; if Lean.Syntax.isOfKind discr `«term[_]» = true then let discr_3 := Lean.Syntax.getArg discr 0; let discr_4 := Lean.Syntax.getArg discr 1; let discr := Lean.Syntax.getArg discr 2; let xs := { elemsAndSeps := Lean.Syntax.getArgs discr_4 }; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `«term#[_,]» #[Lean.Syntax.atom info "#[", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] xs.elemsAndSeps), Lean.Syntax.atom info "]"]) else let discr := Lean.Syntax.getArg discr_2 0; throw () else let discr := Lean.Syntax.getArg discr 1; throw () else let discr := _fun_discr; throw ()

source

def unexpandProdMk :

Lean.PrettyPrinter.Unexpander

Equations

unexpandProdMk _fun_discr = let discr := _fun_discr; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.app = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_2 2 = true then let discr := Lean.Syntax.getArg discr_2 0; let discr_3 := Lean.Syntax.getArg discr_2 1; if Lean.Syntax.isOfKind discr_3 `Lean.Parser.Term.paren = true then let discr_4 := Lean.Syntax.getArg discr_3 0; let discr_5 := Lean.Syntax.getArg discr_3 1; if Lean.Syntax.matchesNull discr_5 2 = true then let discr_6 := Lean.Syntax.getArg discr_5 0; let discr_7 := Lean.Syntax.getArg discr_5 1; if Lean.Syntax.matchesNull discr_7 1 = true then let discr_8 := Lean.Syntax.getArg discr_7 0; if Lean.Syntax.isOfKind discr_8 `Lean.Parser.Term.tupleTail = true then let discr_9 := Lean.Syntax.getArg discr_8 0; let discr_10 := Lean.Syntax.getArg discr_8 1; let discr_11 := Lean.Syntax.getArg discr_3 2; let ys := { elemsAndSeps := Lean.Syntax.getArgs discr_10 }; let y := discr_6; let x := discr; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[x, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.tupleTail #[Lean.Syntax.atom info ",", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[y, Lean.Syntax.atom info ","] ys.elemsAndSeps)]]], Lean.Syntax.atom info ")"]) else let discr_9 := Lean.Syntax.getArg discr_7 0; let discr_10 := Lean.Syntax.getArg discr_3 2; let y := discr_3; let x := discr; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[x, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.tupleTail #[Lean.Syntax.atom info ",", Lean.Syntax.node Lean.SourceInfo.none `null #[y]]]], Lean.Syntax.atom info ")"]) else let discr_8 := Lean.Syntax.getArg discr_5 1; let discr_9 := Lean.Syntax.getArg discr_3 2; let y := discr_3; let x := discr; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[x, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.tupleTail #[Lean.Syntax.atom info ",", Lean.Syntax.node Lean.SourceInfo.none `null #[y]]]], Lean.Syntax.atom info ")"]) else let discr_6 := Lean.Syntax.getArg discr_3 1; let discr_7 := Lean.Syntax.getArg discr_3 2; let y := discr_3; let x := discr; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[x, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.tupleTail #[Lean.Syntax.atom info ",", Lean.Syntax.node Lean.SourceInfo.none `null #[y]]]], Lean.Syntax.atom info ")"]) else let discr_4 := Lean.Syntax.getArg discr_2 1; let y := discr_4; let x := discr; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[x, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.tupleTail #[Lean.Syntax.atom info ",", Lean.Syntax.node Lean.SourceInfo.none `null #[y]]]], Lean.Syntax.atom info ")"]) else let discr := Lean.Syntax.getArg discr 1; throw () else let discr := _fun_discr; throw ()

source

def unexpandIte :

Lean.PrettyPrinter.Unexpander

Equations

unexpandIte _fun_discr = let discr := _fun_discr; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.app = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_2 3 = true then let discr := Lean.Syntax.getArg discr_2 0; let discr_3 := Lean.Syntax.getArg discr_2 1; let discr_4 := Lean.Syntax.getArg discr_2 2; let e := discr_4; let t := discr_3; let c := discr; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `termIfThenElse #[Lean.Syntax.atom info "if", c, Lean.Syntax.atom info "then", t, Lean.Syntax.atom info "else", e]) else let discr := Lean.Syntax.getArg discr 1; throw () else let discr := _fun_discr; throw ()

source

def unexpandSorryAx :

Lean.PrettyPrinter.Unexpander

Equations

unexpandSorryAx _fun_discr = let discr := _fun_discr; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.app = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_2 1 = true then let discr := Lean.Syntax.getArg discr_2 0; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.hole = true then let discr := Lean.Syntax.getArg discr 0; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.sorry #[Lean.Syntax.atom info "sorry"]) else let discr := Lean.Syntax.getArg discr_2 0; throw () else let discr_3 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_3 2 = true then let discr := Lean.Syntax.getArg discr_3 0; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.hole = true then let discr := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr_3 1; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.hole = true then let discr := Lean.Syntax.getArg discr 0; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.sorry #[Lean.Syntax.atom info "sorry"]) else let discr := Lean.Syntax.getArg discr_3 1; throw () else let discr := Lean.Syntax.getArg discr_3 0; let discr := Lean.Syntax.getArg discr_3 1; throw () else let discr := Lean.Syntax.getArg discr 1; throw () else let discr := _fun_discr; throw ()

source

def unexpandEqNDRec :

Lean.PrettyPrinter.Unexpander

Equations

unexpandEqNDRec _fun_discr = let discr := _fun_discr; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.app = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_2 2 = true then let discr := Lean.Syntax.getArg discr_2 0; let discr_3 := Lean.Syntax.getArg discr_2 1; let h := discr_3; let m := discr; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.subst #[h, Lean.Syntax.atom info "▸", Lean.Syntax.node Lean.SourceInfo.none `null #[m]]) else let discr := Lean.Syntax.getArg discr 1; throw () else let discr := _fun_discr; throw ()

source

def unexpandEqRec :

Lean.PrettyPrinter.Unexpander

Equations

unexpandEqRec _fun_discr = let discr := _fun_discr; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.app = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_2 2 = true then let discr := Lean.Syntax.getArg discr_2 0; let discr_3 := Lean.Syntax.getArg discr_2 1; let h := discr_3; let m := discr; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.subst #[h, Lean.Syntax.atom info "▸", Lean.Syntax.node Lean.SourceInfo.none `null #[m]]) else let discr := Lean.Syntax.getArg discr 1; throw () else let discr := _fun_discr; throw ()

source

def unexpandExists :

Lean.PrettyPrinter.Unexpander

Equations

unexpandExists _fun_discr = let discr := _fun_discr; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.app = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_2 1 = true then let discr := Lean.Syntax.getArg discr_2 0; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.fun = true then let discr_3 := Lean.Syntax.getArg discr 0; let discr_4 := Lean.Syntax.getArg discr 1; if Lean.Syntax.isOfKind discr_4 `Lean.Parser.Term.basicFun = true then let discr := Lean.Syntax.getArg discr_4 0; if Lean.Syntax.matchesNull discr 1 = true then let discr_5 := Lean.Syntax.getArg discr 0; cond (Lean.Syntax.isOfKind discr_5 `ident) (let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; if Lean.Syntax.isOfKind discr `«term∃_,_» = true then let discr_6 := Lean.Syntax.getArg discr 0; let discr_7 := Lean.Syntax.getArg discr 1; if Lean.Syntax.isOfKind discr_7 `Lean.explicitBinders = true then let discr_8 := Lean.Syntax.getArg discr_7 0; if Lean.Syntax.isOfKind discr_8 `Lean.unbracketedExplicitBinders = true then let discr_9 := Lean.Syntax.getArg discr_8 0; let discr_10 := Lean.Syntax.getArg discr_8 1; if Lean.Syntax.matchesNull discr_10 0 = true then let discr_11 := Lean.Syntax.getArg discr 2; let discr := Lean.Syntax.getArg discr 3; let b := discr; let xs := Lean.Syntax.getArgs discr_9; let x := discr_5; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `«term∃_,_» #[Lean.Syntax.atom info "∃", Lean.Syntax.node Lean.SourceInfo.none `Lean.explicitBinders #[Lean.Syntax.node Lean.SourceInfo.none `Lean.unbracketedExplicitBinders #[Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[Lean.Syntax.node Lean.SourceInfo.none `Lean.binderIdent #[x]] xs), Lean.Syntax.node Lean.SourceInfo.none `null #[]]], Lean.Syntax.atom info ",", b]) else let discr_11 := Lean.Syntax.getArg discr_8 1; let discr_12 := Lean.Syntax.getArg discr 2; let discr_13 := Lean.Syntax.getArg discr 3; let b := discr; let x := discr_5; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `«term∃_,_» #[Lean.Syntax.atom info "∃", Lean.Syntax.node Lean.SourceInfo.none `Lean.explicitBinders #[Lean.Syntax.node Lean.SourceInfo.none `Lean.unbracketedExplicitBinders #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.binderIdent #[x]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]], Lean.Syntax.atom info ",", b]) else let discr_9 := Lean.Syntax.getArg discr_7 0; let discr_10 := Lean.Syntax.getArg discr 2; let discr_11 := Lean.Syntax.getArg discr 3; let b := discr; let x := discr_5; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `«term∃_,_» #[Lean.Syntax.atom info "∃", Lean.Syntax.node Lean.SourceInfo.none `Lean.explicitBinders #[Lean.Syntax.node Lean.SourceInfo.none `Lean.unbracketedExplicitBinders #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.binderIdent #[x]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]], Lean.Syntax.atom info ",", b]) else let discr_8 := Lean.Syntax.getArg discr 1; let discr_9 := Lean.Syntax.getArg discr 2; let discr_10 := Lean.Syntax.getArg discr 3; let b := discr; let x := discr_5; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `«term∃_,_» #[Lean.Syntax.atom info "∃", Lean.Syntax.node Lean.SourceInfo.none `Lean.explicitBinders #[Lean.Syntax.node Lean.SourceInfo.none `Lean.unbracketedExplicitBinders #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.binderIdent #[x]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]], Lean.Syntax.atom info ",", b]) else let discr := Lean.Syntax.getArg discr_4 2; let b := discr; let x := discr_5; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `«term∃_,_» #[Lean.Syntax.atom info "∃", Lean.Syntax.node Lean.SourceInfo.none `Lean.explicitBinders #[Lean.Syntax.node Lean.SourceInfo.none `Lean.unbracketedExplicitBinders #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.binderIdent #[x]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]], Lean.Syntax.atom info ",", b])) (let discr_6 := Lean.Syntax.getArg discr 0; if Lean.Syntax.isOfKind discr_6 `Lean.Parser.Term.paren = true then let discr := Lean.Syntax.getArg discr_6 0; let discr := Lean.Syntax.getArg discr_6 1; if Lean.Syntax.matchesNull discr 2 = true then let discr_7 := Lean.Syntax.getArg discr 0; cond (Lean.Syntax.isOfKind discr_7 `ident) (let discr_8 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_8 1 = true then let discr := Lean.Syntax.getArg discr_8 0; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.typeAscription = true then let discr_9 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let discr_10 := Lean.Syntax.getArg discr_6 2; let discr_11 := Lean.Syntax.getArg discr_4 1; let discr_12 := Lean.Syntax.getArg discr_4 2; let b := discr_12; let t := discr; let x := discr_7; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `«term∃_,_» #[Lean.Syntax.atom info "∃", Lean.Syntax.node Lean.SourceInfo.none `Lean.explicitBinders #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.bracketedExplicitBinders #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.binderIdent #[x]], Lean.Syntax.atom info ":", t, Lean.Syntax.atom info ")"]]], Lean.Syntax.atom info ",", b]) else let discr := Lean.Syntax.getArg discr_8 0; let discr := Lean.Syntax.getArg discr_6 2; let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; throw () else let discr := Lean.Syntax.getArg discr 1; let discr := Lean.Syntax.getArg discr_6 2; let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; throw ()) (let discr_8 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let discr := Lean.Syntax.getArg discr_6 2; let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; throw ()) else let discr := Lean.Syntax.getArg discr_6 1; let discr := Lean.Syntax.getArg discr_6 2; let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; throw () else let discr := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; throw ()) else let discr := Lean.Syntax.getArg discr_4 0; let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; throw () else let discr := Lean.Syntax.getArg discr 1; throw () else let discr := Lean.Syntax.getArg discr_2 0; throw () else let discr := Lean.Syntax.getArg discr 1; throw () else let discr := _fun_discr; throw ()

source

def unexpandSigma :

Lean.PrettyPrinter.Unexpander

Equations

unexpandSigma _fun_discr = let discr := _fun_discr; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.app = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_2 1 = true then let discr := Lean.Syntax.getArg discr_2 0; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.fun = true then let discr_3 := Lean.Syntax.getArg discr 0; let discr_4 := Lean.Syntax.getArg discr 1; if Lean.Syntax.isOfKind discr_4 `Lean.Parser.Term.basicFun = true then let discr := Lean.Syntax.getArg discr_4 0; if Lean.Syntax.matchesNull discr 1 = true then let discr_5 := Lean.Syntax.getArg discr 0; if Lean.Syntax.isOfKind discr_5 `Lean.Parser.Term.paren = true then let discr := Lean.Syntax.getArg discr_5 0; let discr := Lean.Syntax.getArg discr_5 1; if Lean.Syntax.matchesNull discr 2 = true then let discr_6 := Lean.Syntax.getArg discr 0; cond (Lean.Syntax.isOfKind discr_6 `ident) (let discr_7 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_7 1 = true then let discr := Lean.Syntax.getArg discr_7 0; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.typeAscription = true then let discr_8 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let discr_9 := Lean.Syntax.getArg discr_5 2; let discr_10 := Lean.Syntax.getArg discr_4 1; let discr_11 := Lean.Syntax.getArg discr_4 2; let b := discr_11; let t := discr; let x := discr_6; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `«term_×__1» #[Lean.Syntax.node Lean.SourceInfo.none `Lean.bracketedExplicitBinders #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.binderIdent #[x]], Lean.Syntax.atom info ":", t, Lean.Syntax.atom info ")"], Lean.Syntax.atom info "×", b]) else let discr := Lean.Syntax.getArg discr_7 0; let discr := Lean.Syntax.getArg discr_5 2; let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; throw () else let discr := Lean.Syntax.getArg discr 1; let discr := Lean.Syntax.getArg discr_5 2; let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; throw ()) (let discr_7 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let discr := Lean.Syntax.getArg discr_5 2; let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; throw ()) else let discr := Lean.Syntax.getArg discr_5 1; let discr := Lean.Syntax.getArg discr_5 2; let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; throw () else let discr := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; throw () else let discr := Lean.Syntax.getArg discr_4 0; let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; throw () else let discr := Lean.Syntax.getArg discr 1; throw () else let discr := Lean.Syntax.getArg discr_2 0; throw () else let discr := Lean.Syntax.getArg discr 1; throw () else let discr := _fun_discr; throw ()

source

def unexpandPSigma :

Lean.PrettyPrinter.Unexpander

Equations

unexpandPSigma _fun_discr = let discr := _fun_discr; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.app = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_2 1 = true then let discr := Lean.Syntax.getArg discr_2 0; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.fun = true then let discr_3 := Lean.Syntax.getArg discr 0; let discr_4 := Lean.Syntax.getArg discr 1; if Lean.Syntax.isOfKind discr_4 `Lean.Parser.Term.basicFun = true then let discr := Lean.Syntax.getArg discr_4 0; if Lean.Syntax.matchesNull discr 1 = true then let discr_5 := Lean.Syntax.getArg discr 0; if Lean.Syntax.isOfKind discr_5 `Lean.Parser.Term.paren = true then let discr := Lean.Syntax.getArg discr_5 0; let discr := Lean.Syntax.getArg discr_5 1; if Lean.Syntax.matchesNull discr 2 = true then let discr_6 := Lean.Syntax.getArg discr 0; cond (Lean.Syntax.isOfKind discr_6 `ident) (let discr_7 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_7 1 = true then let discr := Lean.Syntax.getArg discr_7 0; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.typeAscription = true then let discr_8 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let discr_9 := Lean.Syntax.getArg discr_5 2; let discr_10 := Lean.Syntax.getArg discr_4 1; let discr_11 := Lean.Syntax.getArg discr_4 2; let b := discr_11; let t := discr; let x := discr_6; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `«term_×'_» #[Lean.Syntax.node Lean.SourceInfo.none `Lean.bracketedExplicitBinders #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.binderIdent #[x]], Lean.Syntax.atom info ":", t, Lean.Syntax.atom info ")"], Lean.Syntax.atom info "×'", b]) else let discr := Lean.Syntax.getArg discr_7 0; let discr := Lean.Syntax.getArg discr_5 2; let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; throw () else let discr := Lean.Syntax.getArg discr 1; let discr := Lean.Syntax.getArg discr_5 2; let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; throw ()) (let discr_7 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let discr := Lean.Syntax.getArg discr_5 2; let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; throw ()) else let discr := Lean.Syntax.getArg discr_5 1; let discr := Lean.Syntax.getArg discr_5 2; let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; throw () else let discr := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; throw () else let discr := Lean.Syntax.getArg discr_4 0; let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; throw () else let discr := Lean.Syntax.getArg discr 1; throw () else let discr := Lean.Syntax.getArg discr_2 0; throw () else let discr := Lean.Syntax.getArg discr 1; throw () else let discr := _fun_discr; throw ()

source

def unexpandSubtype :

Lean.PrettyPrinter.Unexpander

Equations

unexpandSubtype _fun_discr = let discr := _fun_discr; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.app = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_2 1 = true then let discr := Lean.Syntax.getArg discr_2 0; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.fun = true then let discr_3 := Lean.Syntax.getArg discr 0; let discr_4 := Lean.Syntax.getArg discr 1; if Lean.Syntax.isOfKind discr_4 `Lean.Parser.Term.basicFun = true then let discr := Lean.Syntax.getArg discr_4 0; if Lean.Syntax.matchesNull discr 1 = true then let discr_5 := Lean.Syntax.getArg discr 0; if Lean.Syntax.isOfKind discr_5 `Lean.Parser.Term.paren = true then let discr := Lean.Syntax.getArg discr_5 0; let discr := Lean.Syntax.getArg discr_5 1; if Lean.Syntax.matchesNull discr 2 = true then let discr_6 := Lean.Syntax.getArg discr 0; cond (Lean.Syntax.isOfKind discr_6 `ident) (let discr_7 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_7 1 = true then let discr := Lean.Syntax.getArg discr_7 0; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.typeAscription = true then let discr_8 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let discr_9 := Lean.Syntax.getArg discr_5 2; let discr_10 := Lean.Syntax.getArg discr_4 1; let discr_11 := Lean.Syntax.getArg discr_4 2; let p := discr_11; let type := discr; let x := discr_6; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `«term{__:_//_}» #[Lean.Syntax.atom info "{", x, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ":", type], Lean.Syntax.atom info "//", p, Lean.Syntax.atom info "}"]) else let discr := Lean.Syntax.getArg discr_7 0; let discr := Lean.Syntax.getArg discr_5 2; let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; throw () else let discr := Lean.Syntax.getArg discr 1; let discr := Lean.Syntax.getArg discr_5 2; let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; throw ()) (let discr_7 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let discr := Lean.Syntax.getArg discr_5 2; let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; throw ()) else let discr := Lean.Syntax.getArg discr_5 1; let discr := Lean.Syntax.getArg discr_5 2; let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; throw () else let discr_6 := Lean.Syntax.getArg discr 0; cond (Lean.Syntax.isOfKind discr_6 `ident) (let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; let p := discr; let x := discr_6; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `«term{__:_//_}» #[Lean.Syntax.atom info "{", x, Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "//", p, Lean.Syntax.atom info "}"])) (let discr := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; throw ()) else let discr := Lean.Syntax.getArg discr_4 0; let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; throw () else let discr := Lean.Syntax.getArg discr 1; throw () else let discr := Lean.Syntax.getArg discr_2 0; throw () else let discr := Lean.Syntax.getArg discr 1; throw () else let discr := _fun_discr; throw ()

source

def tacticFunext__ :

Lean.ParserDescr

Equations

tacticFunext__ = Lean.ParserDescr.node `tacticFunext__ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "funext " false) (Lean.ParserDescr.unary `many1 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `colGt) (Lean.ParserDescr.cat `term 1024))))

Apply function extensionality and introduce new hypotheses. The tactic funext will keep applying new the funext lemma until the goal target is not reducible to

  |-  ((fun x => ...) = (fun x => ...))

The variant funexth₁...hₙ applies funext n times, and uses the given identifiers to name the new hypotheses. Patterns can be used like in the intro tactic. Example, given a goal

  |-  ((fun x : Nat × Bool => ...) = (fun x => ...))

funext(a,b) applies funext once and performs pattern matching on the newly introduced pair.

source

def «command_ClassAbbrev__:_:=__,» :

Lean.ParserDescr

Equations

«command_ClassAbbrev__:_:=__,» = Lean.ParserDescr.node `«command_ClassAbbrev__:_:=__,» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `declModifiers) (Lean.ParserDescr.symbol "class ")) (Lean.ParserDescr.symbol "abbrev ")) (Lean.ParserDescr.const `declId)) (Lean.ParserDescr.unary `many (Lean.ParserDescr.const `bracketedBinder))) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol ":") (Lean.ParserDescr.cat `term 0)))) (Lean.ParserDescr.symbol ":=")) (Lean.ParserDescr.unary `withPosition (Lean.ParserDescr.unary `many (Lean.ParserDescr.unary `group (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `colGe) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.symbol ",")))))))

source

def «tactic·.__;_» :

Lean.ParserDescr

Equations

«tactic·.__;_» = Lean.ParserDescr.node `«tactic·.__;_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.symbol "·") (Lean.ParserDescr.symbol ".")) (Lean.ParserDescr.const `ppHardSpace)) (Lean.ParserDescr.unary `many1Indent (Lean.ParserDescr.unary `group (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.cat `tactic 0) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.symbol ";"))) (Lean.ParserDescr.const `ppLine)))))

·tac focuses on the main goal and tries to solve it using tac, or else fails.

source

def solve :

Lean.ParserDescr

Equations

solve = Lean.ParserDescr.node `solve 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "solve " false) (Lean.ParserDescr.unary `withPosition (Lean.ParserDescr.unary `many1 (Lean.ParserDescr.unary `group (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `colGe) (Lean.ParserDescr.symbol "|")) (Lean.ParserDescr.const `tacticSeq))))))

Similar to first, but succeeds only if one the given tactics solves the current goal.

source

inductive Lean.Loop :

Type

mk: Lean.Loop

source

@[inline]

def Lean.Loop.forIn {β : Type u} {m : Type u → Type v} [inst : Monad m] :

Lean.Loop → β → (Unit → β → m (ForInStep β)) → m β

Equations

Lean.Loop.forIn x init f = Lean.Loop.forIn.loop f init

source

@[specialize]

partial def Lean.Loop.forIn.loop {β : Type u} {m : Type u → Type v} [inst : Monad m] (f : Unit → β → m (ForInStep β)) (b : β) :

m β

source

instance Lean.instForInLoopUnit {m : Type u_1 → Type u_2} :

ForIn m Lean.Loop Unit

Equations

Lean.instForInLoopUnit = { forIn := fun {β} [Monad m] => Lean.Loop.forIn }

source

def Lean.doElemRepeat_ :

Lean.ParserDescr

Equations

Lean.doElemRepeat_ = Lean.ParserDescr.node `Lean.doElemRepeat_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "repeat ") (Lean.ParserDescr.const `doSeq))

source

def Lean.doElemWhile_Do_ :

Lean.ParserDescr

Equations

Lean.doElemWhile_Do_ = Lean.ParserDescr.node `Lean.doElemWhile_Do_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "while ") (Lean.ParserDescr.const `termBeforeDo)) (Lean.ParserDescr.symbol " do ")) (Lean.ParserDescr.const `doSeq))

source

def Lean.doElemRepeat_Until_ :

Lean.ParserDescr

Equations

Lean.doElemRepeat_Until_ = Lean.ParserDescr.node `Lean.doElemRepeat_Until_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "repeat ") (Lean.ParserDescr.const `doSeq)) (Lean.ParserDescr.symbol " until ")) (Lean.ParserDescr.cat `term 0))

source

def Lean.«term_Matches_|» :

Lean.TrailingParserDescr

Equations

Lean.«term_Matches_|» = Lean.ParserDescr.trailingNode `Lean.«term_Matches_|» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " matches ") (Lean.ParserDescr.sepBy1 (Lean.ParserDescr.cat `term 51) "|" (Lean.ParserDescr.symbol "|")))