max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-19 19:27:52 -08:00
parent 0911936502
commit ff9858aa87
28 changed files with 17992 additions and 15658 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
stage0/src/Init/Data.lean generated
View file

@ -23,3 +23,4 @@ import Init.Data.Range
import Init.Data.Hashable
import Init.Data.OfScientific
import Init.Data.Format
import Init.Data.Stream

100
stage0/src/Init/Data/Stream.lean generated Normal file
View file

@ -0,0 +1,100 @@
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich, Andrew Kent, Leonardo de Moura
-/
prelude
import Init.Data.Array.Subarray
import Init.Data.Range
/-
Streams are used to implement parallel `for` statements.
Example:
```
for x in xs, y in ys do
...
```
is expanded into
```
let mut s := toStream ys
for x in xs do
match Stream.next? s with
| none => break
| some (y, s') =>
s := s'
...
```
-/
class ToStream (collection : Type u) (stream : outParam (Type u)) : Type u where
toStream : collection → stream
export ToStream (toStream)
class Stream (stream : Type u) (value : outParam (Type v)) : Type (max u v) where
next? : stream → Option (value × stream)
/- Helper class for using dot-notation with `Stream`s -/
structure StreamOf (ρ : Type u) where
s : ρ
abbrev streamOf (s : ρ) :=
StreamOf.mk s
@[inline] partial def StreamOf.forIn [Stream ρ α] [Monad m] [Inhabited (m β)] (s : StreamOf ρ) (b : β) (f : α → β → m (ForInStep β)) : m β := do
let rec @[specialize] visit (s : ρ) (b : β) : m β := do
match Stream.next? s with
| some (a, s) => match (← f a b) with
| ForInStep.done b => return b
| ForInStep.yield b => visit s b
| none => return b
visit s.s b
instance : ToStream (List α) (List α) where
toStream c := c
instance : ToStream (Array α) (Subarray α) where
toStream a := a[:a.size]
instance : ToStream (Subarray α) (Subarray α) where
toStream a := a
instance : ToStream String Substring where
toStream s := s.toSubstring
instance : ToStream Std.Range Std.Range where
toStream r := r
instance [Stream ρ α] [Stream γ β] : Stream (ρ × γ) (α × β) where
next? | (s₁, s₂) =>
match Stream.next? s₁ with
| none => none
| some (a, s₁) => match Stream.next? s₂ with
| none => none
| some (b, s₂) => some ((a, b), (s₁, s₂))
instance : Stream (List α) α where
next?
| [] => none
| a::as => some (a, as)
instance : Stream (Subarray α) α where
next? s :=
if h : s.start < s.stop then
have s.start + 1 ≤ s.stop from Nat.succLeOfLt h
some (s.as.get ⟨s.start, Nat.ltOfLtOfLe h s.h₂⟩, { s with start := s.start + 1, h₁ := this })
else
none
instance : Stream Std.Range Nat where
next? r :=
if r.start < r.stop then
some (r.start, { r with start := r.start + r.step })
else
none
instance : Stream Substring Char where
next? s :=
if s.startPos < s.stopPos then
some (s.str.get s.startPos, { s with startPos := s.str.next s.startPos })
else
none

1
stage0/src/Init/Data/ToString/Basic.lean generated
View file

@ -27,7 +27,6 @@ instance {α} [ToString α] : ToString (id α) :=
instance {α} [ToString α] : ToString (Id α) :=
inferInstanceAs (ToString α)
@[defaultInstance low]
instance : ToString String :=
⟨fun s => s⟩

5
stage0/src/Init/Meta.lean generated
View file

@ -21,8 +21,11 @@ def isLetterLike (c : Char) : Bool :=
(0x2100 ≤ c.val && c.val ≤ 0x214f) || -- Letter like block
(0x1d49c ≤ c.val && c.val ≤ 0x1d59f) -- Latin letters, Script, Double-struck, Fractur
def isNumericSubscript (c : Char) : Bool :=
0x2080 ≤ c.val && c.val ≤ 0x2089
def isSubScriptAlnum (c : Char) : Bool :=
(0x2080 ≤ c.val && c.val ≤ 0x2089) || -- numeric subscripts
isNumericSubscript c ||
(0x2090 ≤ c.val && c.val ≤ 0x209c) ||
(0x1d62 ≤ c.val && c.val ≤ 0x1d6a)

35
stage0/src/Lean/Elab/AutoBound.lean generated Normal file
View file

@ -0,0 +1,35 @@
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Data.Options
/- Basic support for auto bound implicit local names -/
namespace Lean.Elab
builtin_initialize
registerOption `autoBoundImplicitLocal {
defValue := true
group := ""
descr := "Unbound local variables in declaration headers become implicit arguments if they are a lower case or greek letter followed by numeric digits. For example, `def f (x : Vector α n) : Vector α n :=` automatically introduces the implicit variables {α n}"
}
def getAutoBoundImplicitLocalOption (opts : Options) : Bool :=
opts.get `autoBoundImplicitLocal true
private def allNumeral (s : Substring) : Bool :=
s.all fun c => c.isDigit || isNumericSubscript c
def isValidAutoBoundImplicitName (n : Name) : Bool :=
match n.eraseMacroScopes with
| Name.str Name.anonymous s _ => s.length > 0 && (isGreek s[0] || s[0].isLower) && allNumeral (s.toSubstring.drop 1)
| _ => false
def isValidAutoBoundLevelName (n : Name) : Bool :=
match n.eraseMacroScopes with
| Name.str Name.anonymous s _ => s.length > 0 && s[0].isLower && allNumeral (s.toSubstring.drop 1)
| _ => false
end Lean.Elab

51
stage0/src/Lean/Elab/Do.lean generated
View file

@ -1297,34 +1297,39 @@ def doUnlessToCode (doSeqToCode : List Syntax → M CodeBlock) (doUnless : Synta
/- Generate `CodeBlock` for `doFor; doElems`
`doFor` is of the form
```
for " >> termParser >> " in " >> termParser >> "do " >> doSeq
def doForDecl := parser! termParser >> " in " >> withForbidden "do" termParser
def doFor := parser! "for " >> sepBy1 doForDecl ", " >> "do " >> doSeq
``` -/
def doForToCode (doSeqToCode : List Syntax → M CodeBlock) (doFor : Syntax) (doElems : List Syntax) : M CodeBlock := do
let ref := doFor
let x := doFor[1]
let xs := doFor[3]
let forElems := getDoSeqElems doFor[5]
let forInBodyCodeBlock ← withFor (doSeqToCode forElems)
let ⟨uvars, forInBody⟩ ← mkForInBody x forInBodyCodeBlock
let uvarsTuple ← liftMacroM $ mkTuple ref (uvars.map (mkIdentFrom ref))
if hasReturn forInBodyCodeBlock.code then
let forInTerm ← `($(xs).forIn (MProd.mk none $uvarsTuple) fun $x (MProd.mk _ $uvarsTuple) => $forInBody)
let auxDo ← `(do let r ← $forInTerm:term;
$uvarsTuple:term := r.2;
match r.1 with
| none => Pure.pure (ensureExpectedType! "type mismatch, 'for'" PUnit.unit)
| some a => return ensureExpectedType! "type mismatch, 'for'" a)
doSeqToCode (getDoSeqElems (getDoSeq auxDo) ++ doElems)
let doForDecls := doFor[1].getArgs
if doForDecls.size > 1 then
throwError! "parallel 'do' not implemented yet"
else
let forInTerm ← `($(xs).forIn $uvarsTuple fun $x $uvarsTuple => $forInBody)
if doElems.isEmpty then
let ref := doFor
let x := doForDecls[0][0]
let xs := doForDecls[0][2]
let forElems := getDoSeqElems doFor[3]
let forInBodyCodeBlock ← withFor (doSeqToCode forElems)
let ⟨uvars, forInBody⟩ ← mkForInBody x forInBodyCodeBlock
let uvarsTuple ← liftMacroM $ mkTuple ref (uvars.map (mkIdentFrom ref))
if hasReturn forInBodyCodeBlock.code then
let forInTerm ← `($(xs).forIn (MProd.mk none $uvarsTuple) fun $x (MProd.mk _ $uvarsTuple) => $forInBody)
let auxDo ← `(do let r ← $forInTerm:term;
$uvarsTuple:term := r;
Pure.pure (ensureExpectedType! "type mismatch, 'for'" PUnit.unit))
doSeqToCode $ getDoSeqElems (getDoSeq auxDo)
else
let auxDo ← `(do let r ← $forInTerm:term; $uvarsTuple:term := r)
$uvarsTuple:term := r.2;
match r.1 with
| none => Pure.pure (ensureExpectedType! "type mismatch, 'for'" PUnit.unit)
| some a => return ensureExpectedType! "type mismatch, 'for'" a)
doSeqToCode (getDoSeqElems (getDoSeq auxDo) ++ doElems)
else
let forInTerm ← `($(xs).forIn $uvarsTuple fun $x $uvarsTuple => $forInBody)
if doElems.isEmpty then
let auxDo ← `(do let r ← $forInTerm:term;
$uvarsTuple:term := r;
Pure.pure (ensureExpectedType! "type mismatch, 'for'" PUnit.unit))
doSeqToCode $ getDoSeqElems (getDoSeq auxDo)
else
let auxDo ← `(do let r ← $forInTerm:term; $uvarsTuple:term := r)
doSeqToCode (getDoSeqElems (getDoSeq auxDo) ++ doElems)
/-- Generate `CodeBlock` for `doMatch; doElems` -/
def doMatchToCode (doSeqToCode : List Syntax → M CodeBlock) (doMatch : Syntax) (doElems: List Syntax) : M CodeBlock := do

7
stage0/src/Lean/Elab/Level.lean generated
View file

@ -6,6 +6,7 @@ Authors: Leonardo de Moura
import Lean.Meta.LevelDefEq
import Lean.Elab.Exception
import Lean.Elab.Log
import Lean.Elab.AutoBound
namespace Lean.Elab.Level
@ -33,17 +34,11 @@ instance : MonadNameGenerator LevelElabM where
setNGen ngen := modify fun s => { s with ngen := ngen }
def mkFreshLevelMVar : LevelElabM Level := do
let mvarId ← mkFreshId
modify fun s => { s with mctx := s.mctx.addLevelMVarDecl mvarId }
return mkLevelMVar mvarId
private def isValidAutoBoundLevelName (n : Name) : Bool :=
match n.eraseMacroScopes with
| Name.str Name.anonymous s _ => s.length == 1 && s[0].isLower
| _ => false
partial def elabLevel (stx : Syntax) : LevelElabM Level := withRef stx do
let kind := stx.getKind
if kind == `Lean.Parser.Level.paren then

301
stage0/src/Lean/Elab/Quotation.lean generated
View file

@ -13,7 +13,7 @@ import Lean.Elab.Quotation.Util
import Lean.Parser.Term
namespace Lean.Elab.Term.Quotation
open Lean.Parser.Term
open Lean.Syntax
open Meta
@ -147,38 +147,47 @@ elabStxQuot! Parser.Term.dynamicQuot
-- an "alternative" of patterns plus right-hand side
private abbrev Alt := List Syntax × Syntax
/-- Information on a pattern's head that influences the compilation of a single
match step. -/
structure BasicHeadInfo where
-- Node kind to match, if any
kind : Option SyntaxNodeKind := none
-- Nested patterns for each argument, if any. In a single match step, we only
-- check that the arity matches. The arity is usually implied by the node kind,
-- but not in the case of `many` nodes.
argPats : Option (Array Syntax) := none
-- Function to apply to the right-hand side in case the match succeeds. Used to
-- bind pattern variables.
rhsFn : Syntax → TermElabM Syntax := pure
/--
In a single match step, we match the first discriminant against the "head" of the first pattern of the first
alternative. This datatype describes what kind of check this involves, which helps other patterns decide if
they are covered by the same check and don't have to be check again (see also `MatchResult`). -/
inductive HeadCheck where
-- match step that always succeeds: _, x, `($x), ...
| unconditional
-- match step based on shape of discriminant
-- If `arity` is given, that amount of new discriminants is introduced. `covered` patterns should then introduce the
-- same amount of new patterns.
-- We actually check the arity at run time only in the case of `null` nodes since it should otherwise by implied by
-- the node kind.
-- without arity: `($x:k)
-- with arity: any quotation without an antiquotation head pattern
| shape (k : SyntaxNodeKind) (arity : Option Nat)
-- other, complicated match step that will probably only cover identical patterns
-- example: antiquotation splices `($[...]*)
| other (pat : Syntax)
inductive HeadInfo where
| basic (bhi : BasicHeadInfo)
| antiquotSplice (stx : Syntax)
open HeadCheck
open HeadInfo
/-- Describe whether a pattern is covered by a head check (induced by the pattern itself or a different pattern). -/
inductive MatchResult where
-- Pattern agrees with head check, remove and transform remaining alternative.
-- If `exhaustive` is `false`, *also* include unchanged alternative in the "no" branch.
| covered (f : Alt → TermElabM Alt) (exhaustive : Bool)
-- Pattern disagrees with head check, include in "no" branch only
| uncovered
-- Pattern is not quite sure yet; include unchanged in both branches
| undecided
instance : Inhabited HeadInfo := ⟨basic {}⟩
open MatchResult
/-- `h1.generalizes h2` iff h1 is equal to or more general than h2, i.e. it matches all nodes
h2 matches. This induces a partial ordering. -/
def HeadInfo.generalizes : HeadInfo → HeadInfo → Bool
| basic { kind := none, .. }, _ => true
| basic { kind := some k1, argPats := none, .. },
basic { kind := some k2, .. } => k1 == k2
| basic { kind := some k1, argPats := some ps1, .. },
basic { kind := some k2, argPats := some ps2, .. } => k1 == k2 && ps1.size == ps2.size
-- roughmost approximation for now
| antiquotSplice stx1, antiquotSplice stx2 => stx1 == stx2
| _, _ => false
/-- All necessary information on a pattern head. -/
structure HeadInfo where
-- check induced by the pattern
check : HeadCheck
-- compute compatibility of pattern with given head check
onMatch (taken : HeadCheck) : MatchResult
-- actually run the specified head check, with the discriminant bound to `discr`
doMatch (yes : (newDiscrs : List Syntax) → TermElabM Syntax) (no : TermElabM Syntax) : TermElabM Syntax
partial def mkTuple : Array Syntax → TermElabM Syntax
| #[] => `(Unit.unit)
@ -187,137 +196,167 @@ partial def mkTuple : Array Syntax → TermElabM Syntax
let stx ← mkTuple (es.eraseIdx 0)
`(Prod.mk $(es[0]) $stx)
private def getHeadInfo (alt : Alt) : HeadInfo :=
let pat := alt.fst.head!;
let unconditional (rhsFn) := basic { rhsFn := rhsFn };
-- variable pattern
if pat.isIdent then unconditional $ fun rhs => `(let $pat := discr; $rhs)
-- wildcard pattern
else if pat.isOfKind `Lean.Parser.Term.hole then unconditional pure
/-- Adapt alternatives that do not introduce new discriminants in `doMatch`, but are covered by those that do so. -/
private def noOpMatchAdaptPats : HeadCheck → Alt → Alt
| shape k (some sz), (pats, rhs) => (List.replicate sz (Unhygienic.run `(_)) ++ pats, rhs)
| _, alt => alt
private def adaptRhs (fn : Syntax → TermElabM Syntax) : Alt → TermElabM Alt
| (pats, rhs) => do (pats, ← fn rhs)
private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
let pat := alt.fst.head!
let unconditionally (rhsFn) := pure {
check := unconditional,
doMatch := fun yes no => yes [],
onMatch := fun taken => covered (adaptRhs rhsFn ∘ noOpMatchAdaptPats taken) (match taken with | unconditional => true | _ => false)
}
-- quotation pattern
else if isQuot pat then
if isQuot pat then
let quoted := getQuotContent pat
if quoted.isAtom then
-- We assume that atoms are uniquely determined by the node kind and never have to be checked
unconditional pure
unconditionally pure
else if isAntiquot quoted && !isEscapedAntiquot quoted then
-- quotation contains a single antiquotation
let k := antiquotKind? quoted;
let k := antiquotKind? quoted |>.get!
-- Antiquotation kinds like `$id:ident` influence the parser, but also need to be considered by
-- match (but not by quotation terms). For example, `($id:ident) and `($e) are not
-- `match` (but not by quotation terms). For example, `($id:ident) and `($e) are not
-- distinguishable without checking the kind of the node to be captured. Note that some
-- antiquotations like the latter one for terms do not correspond to any actual node kind
-- (signified by `k == Name.anonymous`), so we would only check for `ident` here.
--
-- if stx.isOfKind `ident then
-- let id := stx; ...
-- let id := stx; let e := stx; ...
-- else
-- let e := stx; ...
let kind := if k == Name.anonymous then none else k
let anti := getAntiquotTerm quoted
if anti.isIdent then basic { kind := kind, rhsFn := fun rhs => `(let $anti := discr; $rhs) }
else unconditional fun _ => throwErrorAt! anti "match_syntax: antiquotation must be variable {anti}"
else if isAntiquotSuffixSplice quoted then unconditional $ fun _ => throwErrorAt quoted "unexpected antiquotation splice"
else if isAntiquotSplice quoted then unconditional $ fun _ => throwErrorAt quoted "unexpected antiquotation splice"
if anti.isIdent then
let rhsFn := (`(let $anti := discr; $(·)))
if k == Name.anonymous then unconditionally rhsFn else pure {
check := shape k none,
onMatch := fun
| taken@(shape k' sz) =>
if k' == k then
covered (adaptRhs rhsFn ∘ noOpMatchAdaptPats taken) (exhaustive := sz.isNone)
else uncovered
| _ => uncovered,
doMatch := fun yes no => do `(if Syntax.isOfKind discr $(quote k) then $(← yes []) else $(← no)),
}
else throwErrorAt! anti "match_syntax: antiquotation must be variable {anti}"
else if isAntiquotSuffixSplice quoted then throwErrorAt quoted "unexpected antiquotation splice"
else if isAntiquotSplice quoted then throwErrorAt quoted "unexpected antiquotation splice"
else if quoted.getArgs.size == 1 && isAntiquotSuffixSplice quoted[0] then
let anti := getAntiquotTerm (getAntiquotSuffixSpliceInner quoted[0])
unconditional fun rhs => match antiquotSuffixSplice? quoted[0] with
unconditionally fun rhs => match antiquotSuffixSplice? quoted[0] with
| `optional => `(let $anti := Syntax.getOptional? discr; $rhs)
| `many => `(let $anti := Syntax.getArgs discr; $rhs)
| `sepBy => `(let $anti := @SepArray.mk $(getSepFromSplice quoted[0]) (Syntax.getArgs discr); $rhs)
| k => throwErrorAt! quoted "invalid antiquotation suffix splice kind '{k}'"
-- TODO: support for more complex antiquotation splices
else if quoted.getArgs.size == 1 && isAntiquotSplice quoted[0] then
antiquotSplice quoted[0]
else if quoted.getArgs.size == 1 && isAntiquotSplice quoted[0] then pure {
check := other pat,
onMatch := fun
| other pat' => if pat' == pat then covered pure (exhaustive := true) else undecided
| _ => undecided,
doMatch := fun yes no => do
let splice := quoted[0]
let k := antiquotSpliceKind? splice
let contents := getAntiquotSpliceContents splice
let ids ← getAntiquotationIds splice
let yes ← yes []
let no ← no
match k with
| `optional =>
let mut yesMatch := yes
for id in ids do
yesMatch ← `(let $id := some $id; $yesMatch)
let mut yesNoMatch := yes
for id in ids do
yesNoMatch ← `(let $id := none; $yesNoMatch)
`(if discr.isNone then $yesNoMatch
else match discr with
| `($(mkNullNode contents)) => $yesMatch
| _ => $no)
| _ =>
let mut discrs ← `(Syntax.getArgs discr)
if k == `sepBy then
discrs ← `(Array.getSepElems $discrs)
let tuple ← mkTuple ids
let mut yes := yes
let resId ← match ids with
| #[id] => id
| _ =>
for i in [:ids.size] do
let idx := Syntax.mkLit fieldIdxKind (toString (i + 1));
yes ← `(let $(ids[i]) := tuples.map (·.$idx:fieldIdx); $yes)
`(tuples)
`(match ($(discrs).sequenceMap fun
| `($(contents[0])) => some $tuple
| _ => none) with
| some $resId => $yes
| none => $no)
}
else
-- not an antiquotation or escaped antiquotation: match head shape
-- not an antiquotation, or an escaped antiquotation: match head shape
let quoted := unescapeAntiquot quoted
let kind := quoted.getKind
let argPats := quoted.getArgs.map fun arg => Unhygienic.run `(`($(arg)))
basic { kind := quoted.getKind, argPats := argPats }
else
unconditional $ fun _ => throwErrorAt! pat "match_syntax: unexpected pattern kind {pat}"
-- Assuming that the first pattern of the alternative is taken, replace it with patterns (if any) for its
-- child nodes.
-- Ex: `($a + (- $b)) => `($a), `(+), `(- $b)
-- Note: The atom pattern `(+) will be discarded in a later step
private def explodeHeadPat (numArgs : Nat) : HeadInfo × Alt → TermElabM Alt
| (basic info, (pat::pats, rhs)) => do
let newPats := match info.argPats with
| some argPats => argPats.toList
| none => List.replicate numArgs $ Unhygienic.run `(_)
let rhs ← info.rhsFn rhs
pure (newPats ++ pats, rhs)
| (antiquotSplice _, (pat::pats, rhs)) => (pats, rhs)
| _ => unreachable!
pure {
check := shape kind argPats.size,
onMatch := fun taken =>
if (match taken with | shape k' sz => k' == kind && sz == argPats.size | _ => false : Bool) then
covered (fun (pats, rhs) => (argPats.toList ++ pats, rhs)) (exhaustive := true)
else
uncovered,
doMatch := fun yes no => do
let cond ← match kind with
| `null => `(and (Syntax.isOfKind discr $(quote kind)) (BEq.beq (Array.size (Syntax.getArgs discr)) $(quote argPats.size)))
| _ => `(Syntax.isOfKind discr $(quote kind))
let newDiscrs ← (List.range argPats.size).mapM fun i => `(Syntax.getArg discr $(quote i))
`(ite (Eq $cond true) $(← yes newDiscrs) $(← no))
}
else match pat with
| `(_) => unconditionally pure
| `($id:ident) => unconditionally (`(let $id := discr; $(·)))
| `($id:ident@$pat) => do
let info ← getHeadInfo (pat::alt.1.tail!, alt.2)
{ info with onMatch := fun taken => match info.onMatch taken with
| covered f exh => covered (fun alt => f alt >>= adaptRhs (`(let $id := discr; $(·)))) exh
| r => r }
| _ => throwErrorAt! pat "match_syntax: unexpected pattern kind {pat}"
private partial def compileStxMatch (discrs : List Syntax) (alts : List Alt) : TermElabM Syntax := do
trace[Elab.match_syntax]! "match {discrs} with {alts}"
match discrs, alts with
| [], ([], rhs)::_ => pure rhs -- nothing left to match
| _, [] => throwError "non-exhaustive 'match_syntax'"
| discr::discrs, alts => do
let alts := (alts.map getHeadInfo).zip alts;
let (info, alt) := alts.head!
-- introduce pattern matches on the discriminant's children if there are any nested patterns
let newDiscrs ← match info with
| basic { argPats := some pats, .. } => (List.range pats.size).mapM fun i => `(Syntax.getArg discr $(quote i))
| _ => pure []
-- collect matching alternatives and explode them
let yesAlts := alts.filter fun (alt : HeadInfo × Alt) => alt.1.generalizes info
let yesAlts ← yesAlts.mapM $ explodeHeadPat newDiscrs.length
-- NOTE: use fresh macro scopes for recursive call so that different `discr`s introduced by the quotations below do not collide
let yes ← withFreshMacroScope $ compileStxMatch (newDiscrs ++ discrs) yesAlts
let mkNo := do
let noAlts := (alts.filter $ fun (alt : HeadInfo × Alt) => !info.generalizes alt.1).map (·.2)
withFreshMacroScope $ compileStxMatch (discr::discrs) noAlts
match info with
-- unconditional match step
| basic { kind := none, .. } => `(let discr := $discr; $yes)
-- conditional match step
| basic { kind := some kind, argPats := pats, .. } =>
let cond ← match kind, pats with
| `null, some pats => `(and (Syntax.isOfKind discr $(quote kind)) (BEq.beq (Array.size (Syntax.getArgs discr)) $(quote pats.size)))
| _, _ => `(Syntax.isOfKind discr $(quote kind))
let no ← mkNo
`(let discr := $discr; ite (Eq $cond true) $yes $no)
-- terrifying match step
| antiquotSplice splice =>
let k := antiquotSpliceKind? splice
let contents := getAntiquotSpliceContents splice
let ids ← getAntiquotationIds splice
let no ← mkNo
match k with
| `optional =>
let mut yesMatch := yes
for id in ids do
yesMatch ← `(let $id := some $id; $yesMatch)
let mut yesNoMatch := yes
for id in ids do
yesNoMatch ← `(let $id := none; $yesNoMatch)
`(let discr := $discr;
if discr.isNone then $yesNoMatch
else match discr with
| `($(mkNullNode contents)) => $yesMatch
| _ => $no)
| _ =>
let mut discrs ← `(Syntax.getArgs $discr)
if k == `sepBy then
discrs ← `(Array.getSepElems $discrs)
let tuple ← mkTuple ids
let mut yes := yes
let resId ← match ids with
| #[id] => id
| _ =>
for i in [:ids.size] do
let idx := Syntax.mkLit fieldIdxKind (toString (i + 1));
yes ← `(let $(ids[i]) := tuples.map (·.$idx:fieldIdx); $yes)
`(tuples)
`(match ($(discrs).sequenceMap fun
| `($(contents[0])) => some $tuple
| _ => none) with
| some $resId => $yes
| none => $no)
| discr::discrs, alt::alts => do
let info ← getHeadInfo alt
let pat := alt.1.head!
let alts ← (alt::alts).mapM fun alt => do ((← getHeadInfo alt).onMatch info.check, alt)
let m ← info.doMatch
(yes := fun newDiscrs => do
let mut yesAlts ← alts.filterMapM fun
| (covered f _, (_::pats, rhs)) => some <$> f (pats, rhs)
| _ => pure none
let undecidedAlts := alts.filterMap fun
| (undecided, alt) => some alt
| _ => none
if !undecidedAlts.isEmpty then
-- group undecided alternatives in a new default case `| discr2, ... => match discr, discr2, ... with ...`
let vars ← discrs.mapM fun _ => withFreshMacroScope `(discr)
let pats := List.replicate newDiscrs.length (Unhygienic.run `(_)) ++ vars
let alts ← undecidedAlts.toArray.mapM fun alt => `(matchAltExpr| | $(alt.1.toArray),* => $(alt.2))
let rhs ← `(match discr, $[$(vars.toArray):term],* with $alts:matchAlt*)
yesAlts := yesAlts ++ [(pats, rhs)]
withFreshMacroScope $ compileStxMatch (newDiscrs ++ discrs) yesAlts)
(no := do
let nonExhaustiveAlts := alts.filterMap fun
| (covered f (exhaustive := true), alt) => none
| (_, alt) => some alt
withFreshMacroScope $ compileStxMatch (discr::discrs) nonExhaustiveAlts)
`(let discr := $discr; $m)
| _, _ => unreachable!
-- Transform alternatives by binding all right-hand sides to outside the match in order to prevent
@ -344,7 +383,9 @@ def match_syntax.expand (stx : Syntax) : TermElabM Syntax := do
match stx with
| `(match $[$discrs:term],* with $[| $[$patss],* => $rhss]*) => do
-- letBindRhss ...
if patss.all (·.all (!·.isQuot)) then
if !patss.any (·.any (fun
| `($id@$pat) => pat.isQuot
| pat => pat.isQuot)) then
-- no quotations => fall back to regular `match`
throwUnsupportedSyntax
let stx ← compileStxMatch discrs.toList (patss.map (·.toList) |>.zip rhss).toList

8
stage0/src/Lean/Elab/Quotation/Util.lean generated
View file

@ -24,10 +24,10 @@ partial def getAntiquotationIds : Syntax → TermElabM (Array Syntax) :=
partial def getPatternVars (stx : Syntax) : TermElabM (Array Syntax) :=
if stx.isQuot then
getAntiquotationIds stx
else if stx.isIdent then
#[stx]
else
throwErrorAt stx "unsupported pattern in syntax match"
else match stx with
| `($id:ident) => #[id]
| `($id:ident@$e) => do (← getPatternVars e).push id
| _ => throwErrorAt stx "unsupported pattern in syntax match"
partial def getPatternsVars (pats : Array Syntax) : TermElabM (Array Syntax) :=
pats.foldlM (fun vars pat => do return vars ++ (← getPatternVars pat)) #[]

16
stage0/src/Lean/Elab/Term.lean generated
View file

@ -16,6 +16,7 @@ import Lean.Util.RecDepth
import Lean.Elab.Log
import Lean.Elab.Level
import Lean.Elab.Attributes
import Lean.Elab.AutoBound
namespace Lean.Elab.Term
/-
@ -297,16 +298,6 @@ def withLevelNames {α} (levelNames : List Name) (x : TermElabM α) : TermElabM
def withoutErrToSorry {α} (x : TermElabM α) : TermElabM α :=
withReader (fun ctx => { ctx with errToSorry := false }) x
builtin_initialize
registerOption `autoBoundImplicitLocal {
defValue := true
group := ""
descr := "Unbound local variables in declaration headers become implicit arguments if they are a lower case or greek letter. For example, `def f (x : Vector α n) : Vector α n :=` automatically introduces the implicit variables {α n}"
}
private def getAutoBoundImplicitLocalOption (opts : Options) : Bool :=
opts.get `autoBoundImplicitLocal true
/-- Execute `x` with `autoBoundImplicit = (options.get `autoBoundImplicitLocal) && flag` -/
def withAutoBoundImplicitLocal {α} (x : TermElabM α) (flag := true) : TermElabM α := do
let flag := getAutoBoundImplicitLocalOption (← getOptions) && flag
@ -1217,11 +1208,6 @@ private def mkConsts (candidates : List (Name × List String)) (explicitLevels :
let const ← mkConst constName explicitLevels
pure $ (const, projs) :: result
def isValidAutoBoundImplicitName (n : Name) : Bool :=
match n.eraseMacroScopes with
| Name.str Name.anonymous s _ => s.length == 1 && (isGreek s[0] || s[0].isLower)
| _ => false
def resolveName (n : Name) (preresolved : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String)) := do
match (← resolveLocalName n) with
| some (e, projs) =>

2
stage0/src/Lean/Meta/SynthInstance.lean generated
View file

@ -562,6 +562,7 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
trace[Meta.synthInstance]! "FOUND result {result}"
let result ← instantiateMVars result
if (← hasAssignableMVar result) then
trace[Meta.synthInstance]! "Failed has assignable mvar {result.setOption `pp.all true}"
pure none
else
pure (some result)
@ -574,6 +575,7 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
let result ← instantiateMVars result
pure (some result)
else
trace[Meta.synthInstance]! "result type{indentExpr resultType}\nis not definitionally equal to{indentExpr type}"
pure none
if type.hasMVar then
pure result?

5
stage0/src/Lean/Parser/Do.lean generated
View file

@ -83,7 +83,8 @@ def elseIf := atomic (group (withPosition (" else " >> checkLineEq >> " if ")))
>> many (checkColGe "'else if' in 'do' must be indented" >> group (elseIf >> optIdent >> termParser >> " then " >> doSeq))
>> optional (checkColGe "'else' in 'do' must be indented" >> " else " >> doSeq)
@[builtinDoElemParser] def doUnless := parser! "unless " >> withForbidden "do" termParser >> "do " >> doSeq
@[builtinDoElemParser] def doFor := parser! "for " >> termParser >> " in " >> withForbidden "do" termParser >> "do " >> doSeq
def doForDecl := parser! termParser >> " in " >> withForbidden "do" termParser
@[builtinDoElemParser] def doFor := parser! "for " >> sepBy1 doForDecl ", " >> "do " >> doSeq
def doMatchAlts := matchAlts (rhsParser := doSeq)
@[builtinDoElemParser] def doMatch := parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> doMatchAlts
@ -114,7 +115,7 @@ parser is succeeding.
/- macros for using `unless`, `for`, `try`, `return` as terms. They expand into `do unless ...`, `do for ...`, `do try ...`, and `do return ...` -/
@[builtinTermParser] def termUnless := parser! "unless " >> withForbidden "do" termParser >> "do " >> doSeq
@[builtinTermParser] def termFor := parser! "for " >> termParser >> " in " >> withForbidden "do" termParser >> "do " >> doSeq
@[builtinTermParser] def termFor := parser! "for " >> sepBy1 doForDecl ", " >> "do " >> doSeq
@[builtinTermParser] def termTry := parser! "try " >> doSeq >> many (doCatch <|> doCatchMatch) >> optional doFinally
@[builtinTermParser] def termReturn := parser!:leadPrec withPosition ("return " >> optional (checkLineEq >> termParser))

2
stage0/stdlib/CMakeLists.txt generated
View file

File diff suppressed because one or more lines are too long

6
stage0/stdlib/Init/Data.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Data
// Imports: Init.Data.Basic Init.Data.Nat Init.Data.Char Init.Data.String Init.Data.List Init.Data.Int Init.Data.Array Init.Data.ByteArray Init.Data.FloatArray Init.Data.Fin Init.Data.UInt Init.Data.Float Init.Data.Option Init.Data.Random Init.Data.ToString Init.Data.Range Init.Data.Hashable Init.Data.OfScientific Init.Data.Format
// Imports: Init.Data.Basic Init.Data.Nat Init.Data.Char Init.Data.String Init.Data.List Init.Data.Int Init.Data.Array Init.Data.ByteArray Init.Data.FloatArray Init.Data.Fin Init.Data.UInt Init.Data.Float Init.Data.Option Init.Data.Random Init.Data.ToString Init.Data.Range Init.Data.Hashable Init.Data.OfScientific Init.Data.Format Init.Data.Stream
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -32,6 +32,7 @@ lean_object* initialize_Init_Data_Range(lean_object*);
lean_object* initialize_Init_Data_Hashable(lean_object*);
lean_object* initialize_Init_Data_OfScientific(lean_object*);
lean_object* initialize_Init_Data_Format(lean_object*);
lean_object* initialize_Init_Data_Stream(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Data(lean_object* w) {
lean_object * res;
@ -94,6 +95,9 @@ lean_dec_ref(res);
res = initialize_Init_Data_Format(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Stream(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

1078
stage0/stdlib/Init/Data/Stream.c generated Normal file
View file

File diff suppressed because it is too large Load diff

166
stage0/stdlib/Init/Meta.c generated
View file

@ -235,6 +235,7 @@ lean_object* l_Lean_Syntax_copyInfo(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getHeadInfo(lean_object*);
lean_object* l_Lean_Syntax_SepArray_ofElems___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_Meta_0__Lean_Syntax_decodeHexLitAux(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_isNumericSubscript(uint32_t);
lean_object* l_Array_forInUnsafe_loop___at_Lean_mkSepArray___spec__1___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Substring_takeWhileAux___at___private_Init_Meta_0__Lean_Syntax_decodeNameLitAux___spec__2___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_expandInterpolatedStrChunks_match__1(lean_object*);
@ -325,6 +326,7 @@ lean_object* l_Lean_Syntax_copyTailInfo___boxed(lean_object*, lean_object*);
lean_object* l_Lean_mkSepArray(lean_object*, lean_object*);
lean_object* l_Lean_Name_appendBefore_match__1(lean_object*);
lean_object* l___private_Init_Meta_0__Lean_Syntax_decodeNameLitAux(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_isNumericSubscript___boxed(lean_object*);
lean_object* l_Lean_evalOptPrio(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getOptionalIdent_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_termEvalPrec_x21_____closed__5;
@ -542,12 +544,12 @@ lean_object* l___private_Init_Meta_0__Lean_quoteList_match__1___rarg(lean_object
lean_object* l_Array_filterSepElemsM___at_Array_filterSepElems___spec__1___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_Meta_0__Lean_quoteOption_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_monadNameGeneratorLift___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Init_Meta___hyg_4038_(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Init_Meta___hyg_4157_(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Init_Meta___hyg_4388_(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Init_Meta___hyg_4290_(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Init_Meta___hyg_4507_(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Init_Meta___hyg_3940_(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Init_Meta___hyg_4042_(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Init_Meta___hyg_4161_(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Init_Meta___hyg_4392_(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Init_Meta___hyg_4294_(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Init_Meta___hyg_4511_(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Init_Meta___hyg_3944_(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_expandInterpolatedStr___closed__1;
lean_object* l_Lean_Syntax_decodeQuotedChar_match__5(lean_object*);
lean_object* l_Lean_Syntax_expandInterpolatedStr___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -881,87 +883,99 @@ x_4 = lean_box(x_3);
return x_4;
}
}
uint8_t l_Lean_isNumericSubscript(uint32_t x_1) {
_start:
{
uint32_t x_2; uint8_t x_3;
x_2 = 8320;
x_3 = x_2 <= x_1;
if (x_3 == 0)
{
uint8_t x_4;
x_4 = 0;
return x_4;
}
else
{
uint32_t x_5; uint8_t x_6;
x_5 = 8329;
x_6 = x_1 <= x_5;
return x_6;
}
}
}
lean_object* l_Lean_isNumericSubscript___boxed(lean_object* x_1) {
_start:
{
uint32_t x_2; uint8_t x_3; lean_object* x_4;
x_2 = lean_unbox_uint32(x_1);
lean_dec(x_1);
x_3 = l_Lean_isNumericSubscript(x_2);
x_4 = lean_box(x_3);
return x_4;
}
}
uint8_t l_Lean_isSubScriptAlnum(uint32_t x_1) {
_start:
{
uint32_t x_2; lean_object* x_3; uint8_t x_20;
x_2 = 8320;
x_20 = x_2 <= x_1;
if (x_20 == 0)
uint8_t x_2;
x_2 = l_Lean_isNumericSubscript(x_1);
if (x_2 == 0)
{
lean_object* x_21;
x_21 = lean_box(0);
x_3 = x_21;
goto block_19;
uint32_t x_3; uint8_t x_4;
x_3 = 8336;
x_4 = x_3 <= x_1;
if (x_4 == 0)
{
uint32_t x_5; uint8_t x_6;
x_5 = 7522;
x_6 = x_5 <= x_1;
if (x_6 == 0)
{
uint8_t x_7;
x_7 = 0;
return x_7;
}
else
{
uint32_t x_22; uint8_t x_23;
x_22 = 8329;
x_23 = x_1 <= x_22;
if (x_23 == 0)
{
lean_object* x_24;
x_24 = lean_box(0);
x_3 = x_24;
goto block_19;
}
else
{
uint8_t x_25;
x_25 = 1;
return x_25;
}
}
block_19:
{
uint32_t x_4; uint8_t x_5;
lean_dec(x_3);
x_4 = 8336;
x_5 = x_4 <= x_1;
if (x_5 == 0)
{
uint32_t x_6; uint8_t x_7;
x_6 = 7522;
x_7 = x_6 <= x_1;
if (x_7 == 0)
{
uint8_t x_8;
x_8 = 0;
return x_8;
}
else
{
uint32_t x_9; uint8_t x_10;
x_9 = 7530;
x_10 = x_1 <= x_9;
return x_10;
uint32_t x_8; uint8_t x_9;
x_8 = 7530;
x_9 = x_1 <= x_8;
return x_9;
}
}
else
{
uint32_t x_11; uint8_t x_12;
x_11 = 8348;
x_12 = x_1 <= x_11;
if (x_12 == 0)
uint32_t x_10; uint8_t x_11;
x_10 = 8348;
x_11 = x_1 <= x_10;
if (x_11 == 0)
{
uint32_t x_13; uint8_t x_14;
x_13 = 7522;
x_14 = x_13 <= x_1;
if (x_14 == 0)
uint32_t x_12; uint8_t x_13;
x_12 = 7522;
x_13 = x_12 <= x_1;
if (x_13 == 0)
{
uint8_t x_15;
x_15 = 0;
return x_15;
uint8_t x_14;
x_14 = 0;
return x_14;
}
else
{
uint32_t x_16; uint8_t x_17;
x_16 = 7530;
x_17 = x_1 <= x_16;
uint32_t x_15; uint8_t x_16;
x_15 = 7530;
x_16 = x_1 <= x_15;
return x_16;
}
}
else
{
uint8_t x_17;
x_17 = 1;
return x_17;
}
}
}
else
{
uint8_t x_18;
@ -970,8 +984,6 @@ return x_18;
}
}
}
}
}
lean_object* l_Lean_isSubScriptAlnum___boxed(lean_object* x_1) {
_start:
{
@ -8046,7 +8058,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Syntax_strLitToAtom___closed__1;
x_2 = l_Lean_Syntax_strLitToAtom___closed__2;
x_3 = lean_unsigned_to_nat(556u);
x_3 = lean_unsigned_to_nat(559u);
x_4 = lean_unsigned_to_nat(14u);
x_5 = l_Lean_Syntax_strLitToAtom___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -9883,7 +9895,7 @@ return x_75;
}
}
}
lean_object* l_Lean_myMacro____x40_Init_Meta___hyg_3940_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_myMacro____x40_Init_Meta___hyg_3944_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;
@ -10010,7 +10022,7 @@ return x_38;
}
}
}
lean_object* l_Lean_myMacro____x40_Init_Meta___hyg_4038_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_myMacro____x40_Init_Meta___hyg_4042_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;
@ -10221,7 +10233,7 @@ x_1 = l_Lean_termEvalPrec_x21_____closed__7;
return x_1;
}
}
lean_object* l_Lean_myMacro____x40_Init_Meta___hyg_4157_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_myMacro____x40_Init_Meta___hyg_4161_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;
@ -10673,7 +10685,7 @@ return x_75;
}
}
}
lean_object* l_Lean_myMacro____x40_Init_Meta___hyg_4290_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_myMacro____x40_Init_Meta___hyg_4294_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;
@ -10800,7 +10812,7 @@ return x_38;
}
}
}
lean_object* l_Lean_myMacro____x40_Init_Meta___hyg_4388_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_myMacro____x40_Init_Meta___hyg_4392_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;
@ -11011,7 +11023,7 @@ x_1 = l_Lean_termEvalPrio_x21_____closed__7;
return x_1;
}
}
lean_object* l_Lean_myMacro____x40_Init_Meta___hyg_4507_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_myMacro____x40_Init_Meta___hyg_4511_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;

532
stage0/stdlib/Lean/Elab/AutoBound.c generated Normal file
View file

@ -0,0 +1,532 @@
// Lean compiler output
// Module: Lean.Elab.AutoBound
// Imports: Init Lean.Data.Options
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
uint8_t l_Lean_Elab_getAutoBoundImplicitLocalOption(lean_object*);
lean_object* lean_erase_macro_scopes(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
uint8_t l_Lean_Elab_isValidAutoBoundImplicitName(lean_object*);
uint8_t l_String_anyAux_loop(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Char_isDigit(uint32_t);
extern lean_object* l_Lean_instInhabitedParserDescr___closed__1;
lean_object* l_Lean_Elab_isValidAutoBoundLevelName_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_string_utf8_byte_size(lean_object*);
lean_object* l_Lean_Elab_isValidAutoBoundImplicitName_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__3;
uint8_t l_Lean_KVMap_getBool(lean_object*, lean_object*, uint8_t);
lean_object* l___private_Lean_Elab_AutoBound_0__Lean_Elab_allNumeral___lambda__1___boxed(lean_object*);
uint8_t l_Lean_isNumericSubscript(uint32_t);
uint8_t l_Char_isLower(uint32_t);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__1;
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__2;
lean_object* l___private_Lean_Elab_AutoBound_0__Lean_Elab_allNumeral___closed__1;
uint32_t lean_string_utf8_get(lean_object*, lean_object*);
extern lean_object* l_Lean_initFn____x40_Lean_Data_Options___hyg_487____closed__3;
lean_object* l_Substring_nextn(lean_object*, lean_object*, lean_object*);
uint8_t l___private_Lean_Elab_AutoBound_0__Lean_Elab_allNumeral(lean_object*);
lean_object* l_Lean_Elab_isValidAutoBoundImplicitName_match__1(lean_object*);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__4;
lean_object* l___private_Lean_Elab_AutoBound_0__Lean_Elab_allNumeral___boxed(lean_object*);
uint8_t l_Lean_Elab_isValidAutoBoundLevelName(lean_object*);
lean_object* l_Lean_Elab_isValidAutoBoundImplicitName___boxed(lean_object*);
uint8_t l_Lean_isGreek(uint32_t);
uint8_t l___private_Lean_Elab_AutoBound_0__Lean_Elab_allNumeral___lambda__1(uint32_t);
lean_object* lean_register_option(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3_(lean_object*);
lean_object* l_Lean_Elab_isValidAutoBoundLevelName_match__1(lean_object*);
lean_object* lean_string_length(lean_object*);
lean_object* l_Lean_Elab_isValidAutoBoundLevelName___boxed(lean_object*);
lean_object* l_Lean_Elab_getAutoBoundImplicitLocalOption___boxed(lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("autoBoundImplicitLocal");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Unbound local variables in declaration headers become implicit arguments if they are a lower case or greek letter followed by numeric digits. For example, `def f (x : Vector α n) : Vector α n :=` automatically introduces the implicit variables {α n}");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_initFn____x40_Lean_Data_Options___hyg_487____closed__3;
x_2 = l_Lean_instInhabitedParserDescr___closed__1;
x_3 = l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__3;
x_4 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__2;
x_3 = l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__4;
x_4 = lean_register_option(x_2, x_3, x_1);
return x_4;
}
}
uint8_t l_Lean_Elab_getAutoBoundImplicitLocalOption(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; uint8_t x_4;
x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__2;
x_3 = 1;
x_4 = l_Lean_KVMap_getBool(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l_Lean_Elab_getAutoBoundImplicitLocalOption___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l_Lean_Elab_getAutoBoundImplicitLocalOption(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
uint8_t l___private_Lean_Elab_AutoBound_0__Lean_Elab_allNumeral___lambda__1(uint32_t x_1) {
_start:
{
uint8_t x_2;
x_2 = l_Char_isDigit(x_1);
if (x_2 == 0)
{
uint8_t x_3;
x_3 = l_Lean_isNumericSubscript(x_1);
if (x_3 == 0)
{
uint8_t x_4;
x_4 = 1;
return x_4;
}
else
{
uint8_t x_5;
x_5 = 0;
return x_5;
}
}
else
{
uint8_t x_6;
x_6 = 0;
return x_6;
}
}
}
static lean_object* _init_l___private_Lean_Elab_AutoBound_0__Lean_Elab_allNumeral___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Elab_AutoBound_0__Lean_Elab_allNumeral___lambda__1___boxed), 1, 0);
return x_1;
}
}
uint8_t l___private_Lean_Elab_AutoBound_0__Lean_Elab_allNumeral(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; uint8_t x_6;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = lean_ctor_get(x_1, 1);
lean_inc(x_3);
x_4 = lean_ctor_get(x_1, 2);
lean_inc(x_4);
lean_dec(x_1);
x_5 = l___private_Lean_Elab_AutoBound_0__Lean_Elab_allNumeral___closed__1;
x_6 = l_String_anyAux_loop(x_2, x_4, x_5, x_3);
lean_dec(x_4);
lean_dec(x_2);
if (x_6 == 0)
{
uint8_t x_7;
x_7 = 1;
return x_7;
}
else
{
uint8_t x_8;
x_8 = 0;
return x_8;
}
}
}
lean_object* l___private_Lean_Elab_AutoBound_0__Lean_Elab_allNumeral___lambda__1___boxed(lean_object* x_1) {
_start:
{
uint32_t x_2; uint8_t x_3; lean_object* x_4;
x_2 = lean_unbox_uint32(x_1);
lean_dec(x_1);
x_3 = l___private_Lean_Elab_AutoBound_0__Lean_Elab_allNumeral___lambda__1(x_2);
x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* l___private_Lean_Elab_AutoBound_0__Lean_Elab_allNumeral___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l___private_Lean_Elab_AutoBound_0__Lean_Elab_allNumeral(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_isValidAutoBoundImplicitName_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_1) == 1)
{
lean_object* x_4;
x_4 = lean_ctor_get(x_1, 0);
lean_inc(x_4);
if (lean_obj_tag(x_4) == 0)
{
lean_object* x_5; size_t x_6; lean_object* x_7; lean_object* x_8;
lean_dec(x_3);
x_5 = lean_ctor_get(x_1, 1);
lean_inc(x_5);
x_6 = lean_ctor_get_usize(x_1, 2);
lean_dec(x_1);
x_7 = lean_box_usize(x_6);
x_8 = lean_apply_2(x_2, x_5, x_7);
return x_8;
}
else
{
lean_object* x_9;
lean_dec(x_4);
lean_dec(x_2);
x_9 = lean_apply_1(x_3, x_1);
return x_9;
}
}
else
{
lean_object* x_10;
lean_dec(x_2);
x_10 = lean_apply_1(x_3, x_1);
return x_10;
}
}
}
lean_object* l_Lean_Elab_isValidAutoBoundImplicitName_match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Elab_isValidAutoBoundImplicitName_match__1___rarg), 3, 0);
return x_2;
}
}
uint8_t l_Lean_Elab_isValidAutoBoundImplicitName(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_erase_macro_scopes(x_1);
if (lean_obj_tag(x_2) == 1)
{
lean_object* x_3;
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
if (lean_obj_tag(x_3) == 0)
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7;
x_4 = lean_ctor_get(x_2, 1);
lean_inc(x_4);
lean_dec(x_2);
x_5 = lean_string_length(x_4);
x_6 = lean_unsigned_to_nat(0u);
x_7 = lean_nat_dec_lt(x_6, x_5);
lean_dec(x_5);
if (x_7 == 0)
{
uint8_t x_8;
lean_dec(x_4);
x_8 = 0;
return x_8;
}
else
{
uint32_t x_9; uint8_t x_10;
x_9 = lean_string_utf8_get(x_4, x_6);
x_10 = l_Lean_isGreek(x_9);
if (x_10 == 0)
{
uint8_t x_11;
x_11 = l_Char_isLower(x_9);
if (x_11 == 0)
{
uint8_t x_12;
lean_dec(x_4);
x_12 = 0;
return x_12;
}
else
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18;
x_13 = lean_string_utf8_byte_size(x_4);
lean_inc(x_13);
lean_inc(x_4);
x_14 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_14, 0, x_4);
lean_ctor_set(x_14, 1, x_6);
lean_ctor_set(x_14, 2, x_13);
x_15 = lean_unsigned_to_nat(1u);
x_16 = l_Substring_nextn(x_14, x_15, x_6);
lean_dec(x_14);
x_17 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_17, 0, x_4);
lean_ctor_set(x_17, 1, x_16);
lean_ctor_set(x_17, 2, x_13);
x_18 = l___private_Lean_Elab_AutoBound_0__Lean_Elab_allNumeral(x_17);
return x_18;
}
}
else
{
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; uint8_t x_24;
x_19 = lean_string_utf8_byte_size(x_4);
lean_inc(x_19);
lean_inc(x_4);
x_20 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_20, 0, x_4);
lean_ctor_set(x_20, 1, x_6);
lean_ctor_set(x_20, 2, x_19);
x_21 = lean_unsigned_to_nat(1u);
x_22 = l_Substring_nextn(x_20, x_21, x_6);
lean_dec(x_20);
x_23 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_23, 0, x_4);
lean_ctor_set(x_23, 1, x_22);
lean_ctor_set(x_23, 2, x_19);
x_24 = l___private_Lean_Elab_AutoBound_0__Lean_Elab_allNumeral(x_23);
return x_24;
}
}
}
else
{
uint8_t x_25;
lean_dec(x_3);
lean_dec(x_2);
x_25 = 0;
return x_25;
}
}
else
{
uint8_t x_26;
lean_dec(x_2);
x_26 = 0;
return x_26;
}
}
}
lean_object* l_Lean_Elab_isValidAutoBoundImplicitName___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l_Lean_Elab_isValidAutoBoundImplicitName(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_isValidAutoBoundLevelName_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_1) == 1)
{
lean_object* x_4;
x_4 = lean_ctor_get(x_1, 0);
lean_inc(x_4);
if (lean_obj_tag(x_4) == 0)
{
lean_object* x_5; size_t x_6; lean_object* x_7; lean_object* x_8;
lean_dec(x_3);
x_5 = lean_ctor_get(x_1, 1);
lean_inc(x_5);
x_6 = lean_ctor_get_usize(x_1, 2);
lean_dec(x_1);
x_7 = lean_box_usize(x_6);
x_8 = lean_apply_2(x_2, x_5, x_7);
return x_8;
}
else
{
lean_object* x_9;
lean_dec(x_4);
lean_dec(x_2);
x_9 = lean_apply_1(x_3, x_1);
return x_9;
}
}
else
{
lean_object* x_10;
lean_dec(x_2);
x_10 = lean_apply_1(x_3, x_1);
return x_10;
}
}
}
lean_object* l_Lean_Elab_isValidAutoBoundLevelName_match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Elab_isValidAutoBoundLevelName_match__1___rarg), 3, 0);
return x_2;
}
}
uint8_t l_Lean_Elab_isValidAutoBoundLevelName(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_erase_macro_scopes(x_1);
if (lean_obj_tag(x_2) == 1)
{
lean_object* x_3;
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
if (lean_obj_tag(x_3) == 0)
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7;
x_4 = lean_ctor_get(x_2, 1);
lean_inc(x_4);
lean_dec(x_2);
x_5 = lean_string_length(x_4);
x_6 = lean_unsigned_to_nat(0u);
x_7 = lean_nat_dec_lt(x_6, x_5);
lean_dec(x_5);
if (x_7 == 0)
{
uint8_t x_8;
lean_dec(x_4);
x_8 = 0;
return x_8;
}
else
{
uint32_t x_9; uint8_t x_10;
x_9 = lean_string_utf8_get(x_4, x_6);
x_10 = l_Char_isLower(x_9);
if (x_10 == 0)
{
uint8_t x_11;
lean_dec(x_4);
x_11 = 0;
return x_11;
}
else
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; uint8_t x_17;
x_12 = lean_string_utf8_byte_size(x_4);
lean_inc(x_12);
lean_inc(x_4);
x_13 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_13, 0, x_4);
lean_ctor_set(x_13, 1, x_6);
lean_ctor_set(x_13, 2, x_12);
x_14 = lean_unsigned_to_nat(1u);
x_15 = l_Substring_nextn(x_13, x_14, x_6);
lean_dec(x_13);
x_16 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_16, 0, x_4);
lean_ctor_set(x_16, 1, x_15);
lean_ctor_set(x_16, 2, x_12);
x_17 = l___private_Lean_Elab_AutoBound_0__Lean_Elab_allNumeral(x_16);
return x_17;
}
}
}
else
{
uint8_t x_18;
lean_dec(x_3);
lean_dec(x_2);
x_18 = 0;
return x_18;
}
}
else
{
uint8_t x_19;
lean_dec(x_2);
x_19 = 0;
return x_19;
}
}
}
lean_object* l_Lean_Elab_isValidAutoBoundLevelName___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l_Lean_Elab_isValidAutoBoundLevelName(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
lean_object* initialize_Init(lean_object*);
lean_object* initialize_Lean_Data_Options(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Lean_Elab_AutoBound(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Data_Options(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__1();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__1);
l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__2 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__2();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__2);
l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__3 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__3();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__3);
l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__4 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__4();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3____closed__4);
res = l_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_3_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___private_Lean_Elab_AutoBound_0__Lean_Elab_allNumeral___closed__1 = _init_l___private_Lean_Elab_AutoBound_0__Lean_Elab_allNumeral___closed__1();
lean_mark_persistent(l___private_Lean_Elab_AutoBound_0__Lean_Elab_allNumeral___closed__1);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus
}
#endif

1781
stage0/stdlib/Lean/Elab/Do.c generated
View file

File diff suppressed because it is too large Load diff

130
stage0/stdlib/Lean/Elab/Level.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Elab.Level
// Imports: Init Lean.Meta.LevelDefEq Lean.Elab.Exception Lean.Elab.Log
// Imports: Init Lean.Meta.LevelDefEq Lean.Elab.Exception Lean.Elab.Log Lean.Elab.AutoBound
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -17,7 +17,6 @@ lean_object* l_Lean_throwError___at_Lean_Elab_Level_elabLevel___spec__3___boxed(
extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__38;
size_t l_USize_add(size_t, size_t);
lean_object* l_Lean_Elab_Level_instMonadRefLevelElabM;
lean_object* lean_erase_macro_scopes(lean_object*);
lean_object* l_Lean_stringToMessageData(lean_object*);
lean_object* l_Lean_Elab_Level_elabLevel___closed__10;
lean_object* l_Lean_Elab_Level_instMonadNameGeneratorLevelElabM___lambda__1___boxed(lean_object*, lean_object*);
@ -51,7 +50,6 @@ lean_object* l_Lean_Elab_Level_elabLevel___closed__6;
lean_object* l_ReaderT_bind___at_Lean_Elab_Level_instMonadRefLevelElabM___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Subarray_forInUnsafe_loop___at_Lean_Elab_Level_elabLevel___spec__5(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Subarray_forInUnsafe_loop___at_Lean_Elab_Level_elabLevel___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
extern lean_object* l_Lean_Level_LevelToFormat_Result_format___closed__3;
lean_object* l_Subarray_forInUnsafe_loop___at_Lean_Elab_Level_elabLevel___spec__4(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_numLitKind;
@ -60,20 +58,16 @@ lean_object* l_Lean_Elab_Level_mkFreshLevelMVar(lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Level_elabLevel___spec__3(lean_object*, lean_object*, lean_object*);
lean_object* lean_level_mk_max_simp(lean_object*, lean_object*);
lean_object* l_Lean_replaceRef(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Level_0__Lean_Elab_Level_isValidAutoBoundLevelName___boxed(lean_object*);
lean_object* lean_level_mk_imax_simp(lean_object*, lean_object*);
uint8_t l_Char_isLower(uint32_t);
lean_object* l_Lean_Elab_Level_elabLevel_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Level_elabLevel_match__1(lean_object*);
lean_object* l_Lean_Elab_Level_elabLevel_match__2(lean_object*);
lean_object* l_Lean_Syntax_getId(lean_object*);
lean_object* l_Lean_Level_addOffsetAux(lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Level_elabLevel___spec__1(lean_object*, lean_object*, lean_object*);
uint32_t lean_string_utf8_get(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Level_instMonadNameGeneratorLevelElabM___lambda__3(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Level_elabLevel___closed__2;
lean_object* l_Lean_Elab_Level_instMonadRefLevelElabM___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Level_0__Lean_Elab_Level_isValidAutoBoundLevelName_match__1(lean_object*);
lean_object* l_Lean_Elab_Level_elabLevel_match__1___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_KernelException_toMessageData___closed__3;
size_t lean_usize_of_nat(lean_object*);
@ -83,17 +77,16 @@ lean_object* l_Lean_Elab_Level_elabLevel___closed__4;
lean_object* l_Lean_Elab_Level_elabLevel___closed__1;
extern lean_object* l_Lean_identKind;
uint8_t l_List_elem___at_Lean_NameHashSet_insert___spec__2(lean_object*, lean_object*);
uint8_t l_Lean_Elab_isValidAutoBoundLevelName(lean_object*);
lean_object* l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Level_elabLevel___spec__2(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Level_elabLevel___closed__5;
lean_object* l_Lean_Syntax_getArgs(lean_object*);
lean_object* l___private_Lean_Elab_Level_0__Lean_Elab_Level_isValidAutoBoundLevelName_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getKind(lean_object*);
lean_object* l_Lean_mkFreshId___at_Lean_Elab_Level_mkFreshLevelMVar___spec__1___boxed(lean_object*);
lean_object* l_Lean_Elab_Level_elabLevel___closed__3;
lean_object* l_ReaderT_read___at_Lean_Elab_Level_instMonadRefLevelElabM___spec__1(lean_object*, lean_object*);
lean_object* l_Subarray_forInUnsafe_loop___at_Lean_Elab_Level_elabLevel___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_11259____closed__7;
uint8_t l___private_Lean_Elab_Level_0__Lean_Elab_Level_isValidAutoBoundLevelName(lean_object*);
lean_object* l_Lean_Elab_Level_instMonadNameGeneratorLevelElabM___closed__2;
lean_object* l_Lean_Elab_Level_instMonadNameGeneratorLevelElabM___closed__5;
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
@ -102,7 +95,6 @@ lean_object* l_Lean_Elab_Level_instMonadRefLevelElabM___closed__2;
lean_object* l_Lean_mkFreshId___at_Lean_Elab_Level_mkFreshLevelMVar___spec__1___rarg(lean_object*);
lean_object* l_Lean_Elab_Level_instAddMessageContextLevelElabM___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Level_instMonadNameGeneratorLevelElabM___closed__1;
lean_object* lean_string_length(lean_object*);
lean_object* l_Lean_Elab_Level_instMonadRefLevelElabM___closed__1;
lean_object* l_Lean_Level_ofNat(lean_object*);
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
@ -655,116 +647,6 @@ lean_dec(x_1);
return x_3;
}
}
lean_object* l___private_Lean_Elab_Level_0__Lean_Elab_Level_isValidAutoBoundLevelName_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_1) == 1)
{
lean_object* x_4;
x_4 = lean_ctor_get(x_1, 0);
lean_inc(x_4);
if (lean_obj_tag(x_4) == 0)
{
lean_object* x_5; size_t x_6; lean_object* x_7; lean_object* x_8;
lean_dec(x_3);
x_5 = lean_ctor_get(x_1, 1);
lean_inc(x_5);
x_6 = lean_ctor_get_usize(x_1, 2);
lean_dec(x_1);
x_7 = lean_box_usize(x_6);
x_8 = lean_apply_2(x_2, x_5, x_7);
return x_8;
}
else
{
lean_object* x_9;
lean_dec(x_4);
lean_dec(x_2);
x_9 = lean_apply_1(x_3, x_1);
return x_9;
}
}
else
{
lean_object* x_10;
lean_dec(x_2);
x_10 = lean_apply_1(x_3, x_1);
return x_10;
}
}
}
lean_object* l___private_Lean_Elab_Level_0__Lean_Elab_Level_isValidAutoBoundLevelName_match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l___private_Lean_Elab_Level_0__Lean_Elab_Level_isValidAutoBoundLevelName_match__1___rarg), 3, 0);
return x_2;
}
}
uint8_t l___private_Lean_Elab_Level_0__Lean_Elab_Level_isValidAutoBoundLevelName(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_erase_macro_scopes(x_1);
if (lean_obj_tag(x_2) == 1)
{
lean_object* x_3;
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
if (lean_obj_tag(x_3) == 0)
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7;
x_4 = lean_ctor_get(x_2, 1);
lean_inc(x_4);
lean_dec(x_2);
x_5 = lean_string_length(x_4);
x_6 = lean_unsigned_to_nat(1u);
x_7 = lean_nat_dec_eq(x_5, x_6);
lean_dec(x_5);
if (x_7 == 0)
{
uint8_t x_8;
lean_dec(x_4);
x_8 = 0;
return x_8;
}
else
{
lean_object* x_9; uint32_t x_10; uint8_t x_11;
x_9 = lean_unsigned_to_nat(0u);
x_10 = lean_string_utf8_get(x_4, x_9);
lean_dec(x_4);
x_11 = l_Char_isLower(x_10);
return x_11;
}
}
else
{
uint8_t x_12;
lean_dec(x_3);
lean_dec(x_2);
x_12 = 0;
return x_12;
}
}
else
{
uint8_t x_13;
lean_dec(x_2);
x_13 = 0;
return x_13;
}
}
}
lean_object* l___private_Lean_Elab_Level_0__Lean_Elab_Level_isValidAutoBoundLevelName___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l___private_Lean_Elab_Level_0__Lean_Elab_Level_isValidAutoBoundLevelName(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_Level_elabLevel_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -1315,7 +1197,7 @@ else
{
uint8_t x_65;
lean_inc(x_50);
x_65 = l___private_Lean_Elab_Level_0__Lean_Elab_Level_isValidAutoBoundLevelName(x_50);
x_65 = l_Lean_Elab_isValidAutoBoundLevelName(x_50);
if (x_65 == 0)
{
lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; uint8_t x_72;
@ -1863,7 +1745,7 @@ else
{
uint8_t x_204;
lean_inc(x_189);
x_204 = l___private_Lean_Elab_Level_0__Lean_Elab_Level_isValidAutoBoundLevelName(x_189);
x_204 = l_Lean_Elab_isValidAutoBoundLevelName(x_189);
if (x_204 == 0)
{
lean_object* x_205; lean_object* x_206; lean_object* x_207; lean_object* x_208; lean_object* x_209; lean_object* x_210; lean_object* x_211; lean_object* x_212; lean_object* x_213; lean_object* x_214;
@ -2291,6 +2173,7 @@ lean_object* initialize_Init(lean_object*);
lean_object* initialize_Lean_Meta_LevelDefEq(lean_object*);
lean_object* initialize_Lean_Elab_Exception(lean_object*);
lean_object* initialize_Lean_Elab_Log(lean_object*);
lean_object* initialize_Lean_Elab_AutoBound(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Lean_Elab_Level(lean_object* w) {
lean_object * res;
@ -2308,6 +2191,9 @@ lean_dec_ref(res);
res = initialize_Lean_Elab_Log(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Elab_AutoBound(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Level_instMonadRefLevelElabM___closed__1 = _init_l_Lean_Elab_Level_instMonadRefLevelElabM___closed__1();
lean_mark_persistent(l_Lean_Elab_Level_instMonadRefLevelElabM___closed__1);
l_Lean_Elab_Level_instMonadRefLevelElabM___closed__2 = _init_l_Lean_Elab_Level_instMonadRefLevelElabM___closed__2();

23827
stage0/stdlib/Lean/Elab/Quotation.c generated
View file

File diff suppressed because it is too large Load diff

169
stage0/stdlib/Lean/Elab/Quotation/Util.c generated
View file

@ -15,10 +15,12 @@ extern "C" {
#endif
uint8_t l_Lean_Syntax_isQuot(lean_object*);
size_t l_USize_add(size_t, size_t);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
uint8_t l_USize_decEq(size_t, size_t);
lean_object* lean_array_uget(lean_object*, size_t);
lean_object* l_Array_append___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Quotation_getPatternVars___closed__3;
extern lean_object* l_Lean_identKind___closed__2;
extern lean_object* l_Array_empty___closed__1;
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
@ -28,6 +30,7 @@ lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_Quotation_getPatterns
lean_object* l_Lean_Elab_Term_Quotation_getPatternsVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Quotation_getPatternVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Term_Quotation_getAntiquotationIds_go___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Quotation_getPatternVars___closed__5;
lean_object* l_Lean_Elab_Term_Quotation_getPatternVars___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Quotation_getPatternVars___closed__2;
lean_object* l_Lean_replaceRef(lean_object*, lean_object*);
@ -45,14 +48,18 @@ lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Term_Quotation_getAntiquotationI
lean_object* l_Lean_Elab_Term_Quotation_getAntiquotationIds_go___closed__3;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Quotation_getAntiquotationIds___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Quotation_getPatternVars___closed__4;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_2094____closed__2;
lean_object* l_Lean_Elab_Term_Quotation_getAntiquotationIds_go_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Quotation_getAntiquotationIds_go___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Quotation_getAntiquotationIds_go___closed__1;
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Quotation_getPatternsVars___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Term_Quotation_getAntiquotationIds_go___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Quotation_getAntiquotationIds_go___closed__2;
uint8_t l_Lean_Syntax_isEscapedAntiquot(lean_object*);
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
extern lean_object* l_Lean_mkOptionalNode___closed__2;
lean_object* l_Lean_Elab_getBetterRef(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
@ -468,25 +475,43 @@ static lean_object* _init_l_Lean_Elab_Term_Quotation_getPatternVars___closed__1(
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("unsupported pattern in syntax match");
x_1 = lean_mk_string("namedPattern");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_Quotation_getPatternVars___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_Quotation_getPatternVars___closed__1;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_myMacro____x40_Init_Notation___hyg_2094____closed__2;
x_2 = l_Lean_Elab_Term_Quotation_getPatternVars___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Term_Quotation_getPatternVars___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("unsupported pattern in syntax match");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_Quotation_getPatternVars___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_Quotation_getPatternVars___closed__2;
x_1 = l_Lean_Elab_Term_Quotation_getPatternVars___closed__3;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Term_Quotation_getPatternVars___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_Quotation_getPatternVars___closed__4;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
@ -499,35 +524,119 @@ uint8_t x_9;
x_9 = l_Lean_Syntax_isQuot(x_1);
if (x_9 == 0)
{
uint8_t x_10;
x_10 = l_Lean_Syntax_isIdent(x_1);
if (x_10 == 0)
lean_object* x_10; uint8_t x_11;
x_10 = l_Lean_identKind___closed__2;
lean_inc(x_1);
x_11 = l_Lean_Syntax_isOfKind(x_1, x_10);
if (x_11 == 0)
{
lean_object* x_11; lean_object* x_12;
x_11 = l_Lean_Elab_Term_Quotation_getPatternVars___closed__3;
x_12 = l_Lean_throwErrorAt___at_Lean_Elab_Term_Quotation_getAntiquotationIds_go___spec__2(x_1, x_11, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
lean_object* x_12; uint8_t x_13;
x_12 = l_Lean_Elab_Term_Quotation_getPatternVars___closed__2;
lean_inc(x_1);
x_13 = l_Lean_Syntax_isOfKind(x_1, x_12);
if (x_13 == 0)
{
lean_object* x_14; lean_object* x_15;
x_14 = l_Lean_Elab_Term_Quotation_getPatternVars___closed__5;
x_15 = l_Lean_throwErrorAt___at_Lean_Elab_Term_Quotation_getAntiquotationIds_go___spec__2(x_1, x_14, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
lean_dec(x_1);
return x_12;
}
else
{
lean_object* x_13; lean_object* x_14; lean_object* x_15;
lean_dec(x_6);
lean_dec(x_2);
x_13 = l_Lean_mkOptionalNode___closed__2;
x_14 = lean_array_push(x_13, x_1);
x_15 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_8);
return x_15;
}
else
{
lean_object* x_16; lean_object* x_17; uint8_t x_18;
x_16 = lean_unsigned_to_nat(0u);
x_17 = l_Lean_Syntax_getArg(x_1, x_16);
lean_inc(x_17);
x_18 = l_Lean_Syntax_isOfKind(x_17, x_10);
if (x_18 == 0)
{
lean_object* x_19; lean_object* x_20;
lean_dec(x_17);
x_19 = l_Lean_Elab_Term_Quotation_getPatternVars___closed__5;
x_20 = l_Lean_throwErrorAt___at_Lean_Elab_Term_Quotation_getAntiquotationIds_go___spec__2(x_1, x_19, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
lean_dec(x_1);
return x_20;
}
else
{
lean_object* x_16;
x_16 = l_Lean_Elab_Term_Quotation_getAntiquotationIds(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_21 = lean_unsigned_to_nat(2u);
x_22 = l_Lean_Syntax_getArg(x_1, x_21);
lean_dec(x_1);
return x_16;
x_23 = l_Lean_Elab_Term_Quotation_getPatternVars(x_22, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
if (lean_obj_tag(x_23) == 0)
{
uint8_t x_24;
x_24 = !lean_is_exclusive(x_23);
if (x_24 == 0)
{
lean_object* x_25; lean_object* x_26;
x_25 = lean_ctor_get(x_23, 0);
x_26 = lean_array_push(x_25, x_17);
lean_ctor_set(x_23, 0, x_26);
return x_23;
}
else
{
lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30;
x_27 = lean_ctor_get(x_23, 0);
x_28 = lean_ctor_get(x_23, 1);
lean_inc(x_28);
lean_inc(x_27);
lean_dec(x_23);
x_29 = lean_array_push(x_27, x_17);
x_30 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_30, 0, x_29);
lean_ctor_set(x_30, 1, x_28);
return x_30;
}
}
else
{
uint8_t x_31;
lean_dec(x_17);
x_31 = !lean_is_exclusive(x_23);
if (x_31 == 0)
{
return x_23;
}
else
{
lean_object* x_32; lean_object* x_33; lean_object* x_34;
x_32 = lean_ctor_get(x_23, 0);
x_33 = lean_ctor_get(x_23, 1);
lean_inc(x_33);
lean_inc(x_32);
lean_dec(x_23);
x_34 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_34, 0, x_32);
lean_ctor_set(x_34, 1, x_33);
return x_34;
}
}
}
}
}
else
{
lean_object* x_35; lean_object* x_36; lean_object* x_37;
lean_dec(x_6);
lean_dec(x_2);
x_35 = l_Lean_mkOptionalNode___closed__2;
x_36 = lean_array_push(x_35, x_1);
x_37 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_37, 0, x_36);
lean_ctor_set(x_37, 1, x_8);
return x_37;
}
}
else
{
lean_object* x_38;
x_38 = l_Lean_Elab_Term_Quotation_getAntiquotationIds(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
lean_dec(x_1);
return x_38;
}
}
}
@ -713,6 +822,10 @@ l_Lean_Elab_Term_Quotation_getPatternVars___closed__2 = _init_l_Lean_Elab_Term_Q
lean_mark_persistent(l_Lean_Elab_Term_Quotation_getPatternVars___closed__2);
l_Lean_Elab_Term_Quotation_getPatternVars___closed__3 = _init_l_Lean_Elab_Term_Quotation_getPatternVars___closed__3();
lean_mark_persistent(l_Lean_Elab_Term_Quotation_getPatternVars___closed__3);
l_Lean_Elab_Term_Quotation_getPatternVars___closed__4 = _init_l_Lean_Elab_Term_Quotation_getPatternVars___closed__4();
lean_mark_persistent(l_Lean_Elab_Term_Quotation_getPatternVars___closed__4);
l_Lean_Elab_Term_Quotation_getPatternVars___closed__5 = _init_l_Lean_Elab_Term_Quotation_getPatternVars___closed__5();
lean_mark_persistent(l_Lean_Elab_Term_Quotation_getPatternVars___closed__5);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

332
stage0/stdlib/Lean/Elab/Term.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Elab.Term
// Imports: Init Lean.ResolveName Lean.Util.Sorry Lean.Structure Lean.Meta.ExprDefEq Lean.Meta.AppBuilder Lean.Meta.SynthInstance Lean.Meta.CollectMVars Lean.Meta.Tactic.Util Lean.Hygiene Lean.Util.RecDepth Lean.Elab.Log Lean.Elab.Level Lean.Elab.Attributes
// Imports: Init Lean.ResolveName Lean.Util.Sorry Lean.Structure Lean.Meta.ExprDefEq Lean.Meta.AppBuilder Lean.Meta.SynthInstance Lean.Meta.CollectMVars Lean.Meta.Tactic.Util Lean.Hygiene Lean.Util.RecDepth Lean.Elab.Log Lean.Elab.Level Lean.Elab.Attributes Lean.Elab.AutoBound
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -49,6 +49,7 @@ lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFnsAux___
lean_object* l_Lean_Elab_Term_tryPostponeIfHasMVars_match__1(lean_object*);
lean_object* l_Lean_Elab_Term_elabScientificLit___closed__2;
lean_object* l_Lean_Expr_mvarId_x21(lean_object*);
uint8_t l_Lean_Elab_getAutoBoundImplicitLocalOption(lean_object*);
lean_object* l_Nat_foldM_loop___at_Lean_Elab_Term_mkFreshLevelMVars___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoe_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_forIn___at_Lean_Elab_Term_addAutoBoundImplicits___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -58,7 +59,6 @@ lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_instMonadLogTermElabM___closed__2;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_isExplicitApp___boxed(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabBadCDot___closed__2;
lean_object* lean_erase_macro_scopes(lean_object*);
lean_object* l_ReaderT_read___at_Lean_Elab_Term_instMonadLogTermElabM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__11;
lean_object* l_Lean_stringToMessageData(lean_object*);
@ -90,7 +90,6 @@ lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_exceptionToSorry_match
extern lean_object* l_term_x5b___x5d___closed__9;
lean_object* l_Lean_Elab_Term_resolveName___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabProp___closed__3;
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__1;
lean_object* l_List_toString___at_Lean_resolveGlobalConstNoOverload___spec__2(lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_exceptionToSorry___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
@ -115,7 +114,6 @@ lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21_match__1___rarg(lean_object*,
lean_object* l_Array_append___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___closed__2;
lean_object* l_Lean_Elab_Term_throwErrorIfErrors___closed__1;
lean_object* l_Lean_Elab_Term_isValidAutoBoundImplicitName_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_liftAttrM(lean_object*);
lean_object* l_Lean_Elab_Term_throwErrorIfErrors___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_getDeclName_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -128,6 +126,7 @@ extern lean_object* l_Lean_Elab_throwUnsupportedSyntax___rarg___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Term_elabRawNatLit(lean_object*);
extern lean_object* l_Lean_LocalContext_fvarIdToDecl___default___closed__1;
lean_object* l_Lean_getConstInfo___at_Lean_Elab_Term_mkConst___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Elab_isValidAutoBoundImplicitName(lean_object*);
lean_object* l_Lean_Elab_Term_resolveLocalName_loop___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_tryPostponeIfNoneOrMVar_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_resolveLocalName(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -138,7 +137,6 @@ lean_object* l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf___closed__1;
lean_object* l_Lean_Elab_Term_elabNumLit___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabTypeStx___closed__3;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_mkFreshTypeMVarFor___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__4;
lean_object* l_Lean_Elab_Term_registerCustomErrorIfMVar_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_mkTermElabAttributeUnsafe___closed__1;
lean_object* l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabNumLit___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -231,13 +229,13 @@ lean_object* l_Lean_Meta_withLocalDecl___at___private_Lean_Elab_Term_0__Lean_Ela
lean_object* l_Lean_Meta_mkAppM___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_ensureType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabBadCDot___boxed(lean_object*, lean_object*);
uint8_t l_Lean_Elab_Term_isValidAutoBoundImplicitName(lean_object*);
lean_object* l_Lean_MessageData_ofList(lean_object*);
extern lean_object* l_Lean_Elab_logException___rarg___lambda__1___closed__2;
lean_object* l_Lean_Elab_Term_liftLevelM_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_TermElabM_run___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_map___at_Lean_resolveGlobalConst___spec__2(lean_object*);
lean_object* l_Lean_Elab_Term_applyAttributesAt(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__3;
lean_object* l___regBuiltin_Lean_Elab_Term_elabDoubleQuotedName___closed__1;
lean_object* l_ReaderT_bind___at_Lean_Meta_instMonadLCtxMetaM___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_instInhabitedTermElabResult___closed__1;
@ -280,6 +278,7 @@ lean_object* l_Lean_Elab_Term_instMonadMacroAdapterTermElabM___closed__2;
lean_object* l_Lean_Elab_Term_getMainModule___rarg(lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_instMetaEvalTermElabM___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_instMonadMacroAdapterTermElabM___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__5;
uint8_t l_USize_decLt(size_t, size_t);
lean_object* l_Lean_Elab_Term_elabScientificLit___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_instMonadMacroAdapterTermElabM___closed__5;
@ -296,7 +295,6 @@ lean_object* l_Lean_throwError___at_Lean_Elab_Term_elabNumLit___spec__2___boxed(
lean_object* l___regBuiltin_Lean_Elab_Term_elabDoubleQuotedName___closed__2;
lean_object* l_Lean_Elab_Term_elabNumLit_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabTypeWithAutoBoundImplicit___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__2;
extern lean_object* l_Lean_levelZero;
lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Term_elabDoubleQuotedName___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabStrLit___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -358,7 +356,6 @@ lean_object* l_Lean_Elab_Term_elabLevel(lean_object*, lean_object*, lean_object*
lean_object* l_Lean_Elab_Term_mkTermElabAttributeUnsafe(lean_object*);
lean_object* l_Std_PersistentArray_forMAux___at_Lean_Elab_Term_instMetaEvalTermElabM___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_addAutoBoundImplicits___spec__1___closed__4;
lean_object* l_Lean_Elab_Term_isValidAutoBoundImplicitName___boxed(lean_object*);
lean_object* l_Lean_Syntax_isCharLit_x3f(lean_object*);
lean_object* l_Lean_Elab_Term_elabTermEnsuringType(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
@ -410,6 +407,7 @@ lean_object* l_Lean_Elab_Term_MVarErrorInfo_logError___boxed(lean_object*, lean_
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoeSort(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_TermElabM_run(lean_object*);
uint8_t l_Array_contains___at_Lean_Elab_Term_logUnassignedUsingErrorInfos___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7573____closed__1;
lean_object* l_Lean_Elab_Term_MVarErrorInfo_logError___closed__1;
lean_object* l_Lean_Elab_Term_mkTypeMismatchError___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_isExprMVarAssigned___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -423,7 +421,6 @@ lean_object* l___private_Lean_Util_Trace_0__Lean_getResetTraces___at___private_L
lean_object* l_Lean_Elab_Term_mkTypeMismatchError___closed__1;
lean_object* l_Lean_Elab_Term_tryPostponeIfHasMVars_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf___closed__3;
uint8_t l_Lean_KVMap_getBool(lean_object*, lean_object*, uint8_t);
lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___closed__3;
lean_object* l_Lean_Meta_mkHasTypeButIsExpectedMsg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__2;
@ -440,7 +437,6 @@ lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambda(lea
lean_object* l_Lean_Meta_mkAppOptM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_tryPureCoe_x3f___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabQuotedName(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_liftAttrM___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__4;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___lambda__4___closed__1;
extern lean_object* l_Lean_Meta_instMetaEvalMetaM___rarg___closed__2;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -493,7 +489,6 @@ lean_object* l_Lean_Elab_Term_assignLevelMVar(lean_object*, lean_object*, lean_o
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe___closed__5;
lean_object* l_Lean_Elab_Term_resolveLocalName___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_liftAttrM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Char_isLower(uint32_t);
lean_object* l_Lean_Elab_Term_levelMVarToParam___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_strLitKind___closed__2;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___lambda__4___closed__2;
@ -516,7 +511,6 @@ lean_object* l_Lean_Elab_getMacros(lean_object*, lean_object*, lean_object*, lea
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoeSort_match__1___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Array_forInUnsafe_loop___at_Lean_pushScope___spec__1___rarg___lambda__1___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Term_elabBadCDot___closed__3;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_getAutoBoundImplicitLocalOption___boxed(lean_object*);
lean_object* l_Lean_Meta_withMVarContext___at_Lean_Elab_Term_logUnassignedUsingErrorInfos___spec__4(lean_object*);
extern lean_object* l_IO_instInhabitedError___closed__1;
lean_object* l_Lean_resolveGlobalConst___at_Lean_Elab_Term_elabDoubleQuotedName___spec__2___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -525,14 +519,13 @@ lean_object* l_Lean_Elab_Term_mkTypeMismatchError_match__1___rarg(lean_object*,
lean_object* l___regBuiltin_Lean_Elab_Term_elabCharLit(lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabOptLevel___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFnsAux_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5879_(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447_(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5859_(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427_(lean_object*);
lean_object* l_Lean_mkAuxName___at_Lean_Elab_Term_mkAuxName___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_setElabConfig(lean_object*);
lean_object* l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__4;
lean_object* l_Lean_Elab_Term_getLetRecsToLift(lean_object*);
lean_object* l_Lean_Elab_Term_liftLevelM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035_(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_797_(lean_object*);
lean_object* l_Std_PersistentArray_forMAux___at_Lean_Elab_Term_instMetaEvalTermElabM___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getId(lean_object*);
@ -560,7 +553,6 @@ lean_object* l_Lean_Elab_Term_instInhabitedTermElabResult;
lean_object* l_Lean_Elab_Term_resolveName(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoe___closed__2;
lean_object* l_Lean_Elab_Term_instMonadMacroAdapterTermElabM___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__1;
lean_object* l_Lean_Elab_Term_elabProp___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_instMonadLiftTMetaMTermElabM___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_getCurrMacroScope(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -580,10 +572,8 @@ lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_mkFreshTypeMVarFor_mat
extern lean_object* l_Lean_numLitKind___closed__2;
lean_object* l_Std_AssocList_find_x3f___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFns___spec__6___boxed(lean_object*, lean_object*);
lean_object* l_Lean_printTraces___at_Lean_Core_instMetaEvalCoreM___spec__1(lean_object*, lean_object*, lean_object*);
uint32_t lean_string_utf8_get(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_getCurrMacroScope___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_dbg_to_string(lean_object*);
extern lean_object* l_Lean_initFn____x40_Lean_Data_Options___hyg_487____closed__3;
lean_object* l_Lean_Elab_Term_getMessageLog___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_anyMUnsafe_any___at_Lean_Elab_Term_logUnassignedUsingErrorInfos___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabLevel___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -607,7 +597,6 @@ lean_object* l_Lean_Elab_Term_elabProp(lean_object*, lean_object*, lean_object*,
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_addAutoBoundImplicits___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_MVarErrorInfo_logError___closed__5;
lean_object* l_Lean_LocalDecl_toExpr(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__5;
extern lean_object* l_Lean_firstFrontendMacroScope;
lean_object* l___regBuiltin_Lean_Elab_Term_elabTypeOf___closed__3;
lean_object* l_Lean_Elab_mkElabAttribute___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -672,7 +661,6 @@ lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe___closed
lean_object* l_Lean_Elab_Term_tryPostponeIfHasMVars___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_resolveLocalName_loop_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__3;
size_t l_USize_land(size_t, size_t);
lean_object* l_Lean_Elab_Term_mkConst(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_mkSomeContext___closed__2;
@ -681,7 +669,6 @@ lean_object* l_Lean_Elab_Term_mkConst___closed__3;
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_resolveName___closed__4;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoe_match__2(lean_object*);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7640____closed__1;
extern lean_object* l_Lean_nullKind___closed__2;
lean_object* l_Lean_Elab_Term_instMonadLogTermElabM___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__3___rarg(lean_object*);
@ -796,7 +783,6 @@ extern lean_object* l_Lean_KVMap_empty;
lean_object* l_Lean_Syntax_getArgs(lean_object*);
lean_object* l_Lean_Name_append(lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_instMetaEvalTermElabM___spec__11___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_isGreek(uint32_t);
uint8_t l_Lean_BinderInfo_isExplicit(uint8_t);
lean_object* l_Lean_Elab_Term_registerSyntheticMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getKind(lean_object*);
@ -850,7 +836,6 @@ lean_object* l_Lean_throwError___at_Lean_Elab_Term_mkAuxName___spec__1___boxed(l
extern lean_object* l_Lean_instToMessageDataOptionExpr___closed__3;
lean_object* l_Lean_Elab_Term_elabSyntheticHole___closed__6;
lean_object* lean_register_option(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_isValidAutoBoundImplicitName_match__1(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabProp___closed__1;
lean_object* l_Lean_Elab_Term_mkConst___closed__1;
lean_object* l_Lean_Elab_Term_resolveLocalName_loop_match__1(lean_object*);
@ -900,6 +885,7 @@ lean_object* l_List_foldlM___at_Lean_Elab_Term_logUnassignedUsingErrorInfos___sp
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_synthesizeInst_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabDoubleQuotedName(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__2;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFns___closed__3;
lean_object* l___regBuiltin_Lean_Elab_Term_elabEnsureExpectedType___closed__1;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_12387____closed__13;
@ -911,6 +897,7 @@ lean_object* l_Lean_Meta_inferType(lean_object*, lean_object*, lean_object*, lea
lean_object* l_Lean_Elab_Term_elabDoubleQuotedName_match__1___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_mkSorry___rarg___lambda__1___closed__2;
extern lean_object* l_Lean_instInhabitedMessageData___closed__1;
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__1;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambda_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_isExprDefEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MessageLog_forM___at_Lean_Elab_Term_instMetaEvalTermElabM___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -932,9 +919,9 @@ lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Elab_Term_0__Lean_Elab_T
lean_object* l_Lean_Elab_Term_liftCoreM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_evalNat_visit___closed__2;
lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5859____closed__1;
extern size_t l_Std_PersistentHashMap_insertAux___rarg___closed__2;
lean_object* l_Lean_Elab_Term_mkExplicitBinder___closed__1;
uint8_t l___private_Lean_Elab_Term_0__Lean_Elab_Term_getAutoBoundImplicitLocalOption(lean_object*);
lean_object* l_Lean_Elab_Term_registerSyntheticMVarWithCurrRef(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambdaAux(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_logUnassignedUsingErrorInfos(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -947,6 +934,7 @@ lean_object* l_Lean_Elab_Term_getLetRecsToLift___boxed(lean_object*);
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Exception___hyg_3____closed__1;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_MonadEnv_0__Lean_mkAuxNameAux(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__4;
lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_throwTypeMismatchError___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___lambda__4___closed__5;
@ -962,7 +950,6 @@ lean_object* l_Lean_Elab_Term_elabSyntheticHole(lean_object*, lean_object*, lean
lean_object* l_Lean_Elab_Term_TermElabM_toIO_match__1___rarg(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_mkTacticMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_getLevelNames___boxed(lean_object*);
lean_object* lean_string_length(lean_object*);
lean_object* l_Lean_Elab_Term_setMessageLog___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_indentD(lean_object*);
extern lean_object* l_Lean_Elab_unsupportedSyntaxExceptionId;
@ -987,7 +974,7 @@ lean_object* l_IO_println___at_Lean_instEval___spec__1(lean_object*, lean_object
lean_object* l_Lean_Elab_Term_logUnassignedUsingErrorInfos_match__2___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_throwErrorIfErrors(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_NameSet_contains(lean_object*, lean_object*);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7640_(lean_object*);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7573_(lean_object*);
lean_object* l_Lean_Elab_Term_elabByTactic_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_addAutoBoundImplicits(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_withAutoBoundImplicitLocal___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1093,7 +1080,6 @@ lean_object* lean_uint32_to_nat(uint32_t);
lean_object* l___regBuiltin_Lean_Elab_Term_elabSyntheticHole___closed__1;
lean_object* l_Lean_Elab_Term_elabScientificLit_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabByTactic_match__1(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__3;
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_870____closed__2;
lean_object* l_Lean_Elab_Term_elabTypeWithAutoBoundImplicit(lean_object*);
lean_object* l_Lean_Elab_Term_throwTypeMismatchError___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1129,7 +1115,6 @@ lean_object* l_Lean_Elab_Term_elabRawNatLit___boxed(lean_object*, lean_object*,
lean_object* l_Lean_Elab_Term_isMonadApp_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe___closed__7;
lean_object* l_Lean_Elab_Term_elabTermWithoutImplicitLambdas___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5879____closed__1;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFns___closed__2;
lean_object* l_Lean_mkApp3(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_withAutoBoundImplicitLocal___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1157,7 +1142,6 @@ lean_object* l_Lean_Elab_Term_elabNumLit(lean_object*, lean_object*, lean_object
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_findAtAux___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFns___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabCharLit_match__1(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__2;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___closed__1;
uint8_t l_Lean_Syntax_isIdent(lean_object*);
lean_object* l_ReaderT_bind___at_Lean_Elab_Term_instMonadLogTermElabM___spec__2(lean_object*, lean_object*);
@ -2507,7 +2491,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__2;
x_2 = l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__3;
x_3 = lean_unsigned_to_nat(224u);
x_3 = lean_unsigned_to_nat(225u);
x_4 = lean_unsigned_to_nat(14u);
x_5 = l_Lean_Syntax_strLitToAtom___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -4388,83 +4372,13 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Term_withoutErrToSorry___rarg), 8,
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("autoBoundImplicitLocal");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Unbound local variables in declaration headers become implicit arguments if they are a lower case or greek letter. For example, `def f (x : Vector α n) : Vector α n :=` automatically introduces the implicit variables {α n}");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_initFn____x40_Lean_Data_Options___hyg_487____closed__3;
x_2 = l_Lean_instInhabitedParserDescr___closed__1;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__3;
x_4 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__2;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__4;
x_4 = lean_register_option(x_2, x_3, x_1);
return x_4;
}
}
uint8_t l___private_Lean_Elab_Term_0__Lean_Elab_Term_getAutoBoundImplicitLocalOption(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; uint8_t x_4;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__2;
x_3 = 1;
x_4 = l_Lean_KVMap_getBool(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_getAutoBoundImplicitLocalOption___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l___private_Lean_Elab_Term_0__Lean_Elab_Term_getAutoBoundImplicitLocalOption(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_Term_withAutoBoundImplicitLocal___rarg(lean_object* x_1, uint8_t x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_10; uint8_t x_11;
x_10 = lean_ctor_get(x_7, 0);
lean_inc(x_10);
x_11 = l___private_Lean_Elab_Term_0__Lean_Elab_Term_getAutoBoundImplicitLocalOption(x_10);
x_11 = l_Lean_Elab_getAutoBoundImplicitLocalOption(x_10);
lean_dec(x_10);
if (x_11 == 0)
{
@ -9401,7 +9315,7 @@ x_1 = lean_unsigned_to_nat(16u);
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__1() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__1() {
_start:
{
lean_object* x_1;
@ -9409,17 +9323,17 @@ x_1 = lean_mk_string("maxCoeSize");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__2() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__1;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__3() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
@ -9429,7 +9343,7 @@ lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__4() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__4() {
_start:
{
lean_object* x_1;
@ -9437,13 +9351,13 @@ x_1 = lean_mk_string("maximum number of instances used to construct an automatic
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__5() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__3;
x_1 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__3;
x_2 = l_Lean_instInhabitedParserDescr___closed__1;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__4;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__4;
x_4 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -9451,12 +9365,12 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447_(lean_object* x_1) {
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__2;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__5;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__2;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__5;
x_4 = lean_register_option(x_2, x_3, x_1);
return x_4;
}
@ -9465,7 +9379,7 @@ lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_getCoeMaxSize(lean_obj
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__2;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__2;
x_3 = l_Lean_Elab_Term_maxCoeSizeDefault;
x_4 = l_Lean_KVMap_getNat(x_1, x_2, x_3);
return x_4;
@ -28318,7 +28232,7 @@ lean_dec(x_3);
return x_9;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5879____closed__1() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5859____closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -28328,11 +28242,11 @@ x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5879_(lean_object* x_1) {
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5859_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5879____closed__1;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5859____closed__1;
x_3 = l_Lean_registerTraceClass(x_2, x_1);
return x_3;
}
@ -28503,7 +28417,7 @@ lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; lea
x_97 = lean_ctor_get(x_91, 1);
lean_inc(x_97);
lean_dec(x_91);
x_98 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5879____closed__1;
x_98 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5859____closed__1;
x_99 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__2(x_98, x_2, x_3, x_4, x_5, x_6, x_7, x_97);
x_100 = lean_ctor_get(x_99, 0);
lean_inc(x_100);
@ -28545,7 +28459,7 @@ lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean
x_53 = lean_ctor_get(x_47, 1);
lean_inc(x_53);
lean_dec(x_47);
x_54 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5879____closed__1;
x_54 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5859____closed__1;
x_55 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__2(x_54, x_2, x_3, x_4, x_5, x_6, x_7, x_53);
x_56 = lean_ctor_get(x_55, 0);
lean_inc(x_56);
@ -28626,7 +28540,7 @@ x_41 = l_Lean_KernelException_toMessageData___closed__15;
x_42 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_42, 0, x_40);
lean_ctor_set(x_42, 1, x_41);
x_43 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5879____closed__1;
x_43 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5859____closed__1;
x_44 = l_Lean_addTrace___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__1(x_43, x_42, x_2, x_3, x_4, x_5, x_6, x_7, x_36);
x_45 = lean_ctor_get(x_44, 1);
lean_inc(x_45);
@ -28688,7 +28602,7 @@ x_79 = l_Lean_KernelException_toMessageData___closed__15;
x_80 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_80, 0, x_78);
lean_ctor_set(x_80, 1, x_79);
x_81 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5879____closed__1;
x_81 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5859____closed__1;
x_82 = l_Lean_addTrace___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__1(x_81, x_80, x_2, x_3, x_4, x_5, x_6, x_7, x_61);
x_83 = lean_ctor_get(x_82, 1);
lean_inc(x_83);
@ -31426,127 +31340,6 @@ lean_dec(x_4);
return x_10;
}
}
lean_object* l_Lean_Elab_Term_isValidAutoBoundImplicitName_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_1) == 1)
{
lean_object* x_4;
x_4 = lean_ctor_get(x_1, 0);
lean_inc(x_4);
if (lean_obj_tag(x_4) == 0)
{
lean_object* x_5; size_t x_6; lean_object* x_7; lean_object* x_8;
lean_dec(x_3);
x_5 = lean_ctor_get(x_1, 1);
lean_inc(x_5);
x_6 = lean_ctor_get_usize(x_1, 2);
lean_dec(x_1);
x_7 = lean_box_usize(x_6);
x_8 = lean_apply_2(x_2, x_5, x_7);
return x_8;
}
else
{
lean_object* x_9;
lean_dec(x_4);
lean_dec(x_2);
x_9 = lean_apply_1(x_3, x_1);
return x_9;
}
}
else
{
lean_object* x_10;
lean_dec(x_2);
x_10 = lean_apply_1(x_3, x_1);
return x_10;
}
}
}
lean_object* l_Lean_Elab_Term_isValidAutoBoundImplicitName_match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Term_isValidAutoBoundImplicitName_match__1___rarg), 3, 0);
return x_2;
}
}
uint8_t l_Lean_Elab_Term_isValidAutoBoundImplicitName(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_erase_macro_scopes(x_1);
if (lean_obj_tag(x_2) == 1)
{
lean_object* x_3;
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
if (lean_obj_tag(x_3) == 0)
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7;
x_4 = lean_ctor_get(x_2, 1);
lean_inc(x_4);
lean_dec(x_2);
x_5 = lean_string_length(x_4);
x_6 = lean_unsigned_to_nat(1u);
x_7 = lean_nat_dec_eq(x_5, x_6);
lean_dec(x_5);
if (x_7 == 0)
{
uint8_t x_8;
lean_dec(x_4);
x_8 = 0;
return x_8;
}
else
{
lean_object* x_9; uint32_t x_10; uint8_t x_11;
x_9 = lean_unsigned_to_nat(0u);
x_10 = lean_string_utf8_get(x_4, x_9);
lean_dec(x_4);
x_11 = l_Lean_isGreek(x_10);
if (x_11 == 0)
{
uint8_t x_12;
x_12 = l_Char_isLower(x_10);
return x_12;
}
else
{
uint8_t x_13;
x_13 = 1;
return x_13;
}
}
}
else
{
uint8_t x_14;
lean_dec(x_3);
lean_dec(x_2);
x_14 = 0;
return x_14;
}
}
else
{
uint8_t x_15;
lean_dec(x_2);
x_15 = 0;
return x_15;
}
}
}
lean_object* l_Lean_Elab_Term_isValidAutoBoundImplicitName___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l_Lean_Elab_Term_isValidAutoBoundImplicitName(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_Term_resolveName_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -31790,7 +31583,7 @@ else
{
uint8_t x_37;
lean_inc(x_1);
x_37 = l_Lean_Elab_Term_isValidAutoBoundImplicitName(x_1);
x_37 = l_Lean_Elab_isValidAutoBoundImplicitName(x_1);
if (x_37 == 0)
{
lean_object* x_38;
@ -37331,7 +37124,7 @@ x_8 = l_Lean_Elab_Term_instMetaEvalTermElabM___rarg(x_1, x_2, x_3, x_4, x_7, x_6
return x_8;
}
}
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7640____closed__1() {
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7573____closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -37341,7 +37134,7 @@ x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7640_(lean_object* x_1) {
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7573_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -37353,7 +37146,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
lean_dec(x_3);
x_5 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7640____closed__1;
x_5 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7573____closed__1;
x_6 = l_Lean_registerTraceClass(x_5, x_4);
if (lean_obj_tag(x_6) == 0)
{
@ -37426,6 +37219,7 @@ lean_object* initialize_Lean_Util_RecDepth(lean_object*);
lean_object* initialize_Lean_Elab_Log(lean_object*);
lean_object* initialize_Lean_Elab_Level(lean_object*);
lean_object* initialize_Lean_Elab_Attributes(lean_object*);
lean_object* initialize_Lean_Elab_AutoBound(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Lean_Elab_Term(lean_object* w) {
lean_object * res;
@ -37473,6 +37267,9 @@ lean_dec_ref(res);
res = initialize_Lean_Elab_Attributes(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Elab_AutoBound(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Term_Context_declName_x3f___default = _init_l_Lean_Elab_Term_Context_declName_x3f___default();
lean_mark_persistent(l_Lean_Elab_Term_Context_declName_x3f___default);
l_Lean_Elab_Term_Context_macroStack___default = _init_l_Lean_Elab_Term_Context_macroStack___default();
@ -37571,17 +37368,6 @@ if (lean_io_result_is_error(res)) return res;
l_Lean_Elab_Term_termElabAttribute = lean_io_result_get_value(res);
lean_mark_persistent(l_Lean_Elab_Term_termElabAttribute);
lean_dec_ref(res);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__1();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__1);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__2();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__2);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__3 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__3();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__3);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__4 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__4();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035____closed__4);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1035_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Term_throwErrorIfErrors___closed__1 = _init_l_Lean_Elab_Term_throwErrorIfErrors___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_throwErrorIfErrors___closed__1);
l_Lean_Elab_Term_throwErrorIfErrors___closed__2 = _init_l_Lean_Elab_Term_throwErrorIfErrors___closed__2();
@ -37638,17 +37424,17 @@ l_Lean_Elab_Term_synthesizeInstMVarCore___closed__7 = _init_l_Lean_Elab_Term_syn
lean_mark_persistent(l_Lean_Elab_Term_synthesizeInstMVarCore___closed__7);
l_Lean_Elab_Term_maxCoeSizeDefault = _init_l_Lean_Elab_Term_maxCoeSizeDefault();
lean_mark_persistent(l_Lean_Elab_Term_maxCoeSizeDefault);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__1();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__1);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__2();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__2);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__3 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__3();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__3);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__4 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__4();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__4);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__5 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__5();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447____closed__5);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2447_(lean_io_mk_world());
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__1();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__1);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__2();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__2);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__3 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__3();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__3);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__4 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__4();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__4);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__5 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__5();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427____closed__5);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2427_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Term_tryCoeThunk_x3f_match__1___rarg___closed__1 = _init_l_Lean_Elab_Term_tryCoeThunk_x3f_match__1___rarg___closed__1();
@ -37765,9 +37551,9 @@ l_Lean_Elab_Term_mkAuxName___closed__2 = _init_l_Lean_Elab_Term_mkAuxName___clos
lean_mark_persistent(l_Lean_Elab_Term_mkAuxName___closed__2);
l_Lean_Elab_Term_mkAuxName___closed__3 = _init_l_Lean_Elab_Term_mkAuxName___closed__3();
lean_mark_persistent(l_Lean_Elab_Term_mkAuxName___closed__3);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5879____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5879____closed__1();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5879____closed__1);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5879_(lean_io_mk_world());
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5859____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5859____closed__1();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5859____closed__1);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5859_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Term_isLetRecAuxMVar___closed__1 = _init_l_Lean_Elab_Term_isLetRecAuxMVar___closed__1();
@ -37975,9 +37761,9 @@ l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__4 = _init_l_Lean_Elab_Te
lean_mark_persistent(l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__4);
l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__5 = _init_l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__5();
lean_mark_persistent(l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__5);
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7640____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7640____closed__1();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7640____closed__1);
res = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7640_(lean_io_mk_world());
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7573____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7573____closed__1();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7573____closed__1);
res = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7573_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));

26
stage0/stdlib/Lean/Meta/AppBuilder.c generated
View file

@ -72,7 +72,6 @@ lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkHEqTransImp_match__
lean_object* l_Lean_Meta_mkEqRec___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkAppMArgs_loop___closed__2;
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___closed__4;
lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Meta_isLevelDefEqAux___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkAppM___rarg___lambda__1___closed__4;
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkAppOptMAux___closed__2;
@ -140,7 +139,6 @@ lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqSymmImp___closed_
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkDecide(lean_object*);
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkProjectionImp_match__5(lean_object*);
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___closed__5;
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkProjectionImp_match__4(lean_object*);
lean_object* l_Lean_Name_toStringWithSep(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkCongrArgImp___closed__5;
@ -163,6 +161,7 @@ lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkCongrArgImp_match__
extern lean_object* l_Lean_instQuoteBool___closed__5;
lean_object* l_Lean_Meta_mkArbitrary___rarg(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkListLitImp_match__1(lean_object*);
extern lean_object* l_Lean_Meta_synthInstance_x3f___lambda__4___closed__4;
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkCongrFunImp_match__1(lean_object*);
lean_object* l_Lean_Meta_mkAppM___at_Lean_Meta_mkDecideProof___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -3125,23 +3124,6 @@ x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___closed__4() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("\nis not definitionally equal to");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___closed__4;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
@ -3226,7 +3208,7 @@ x_32 = l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___closed__3;
x_33 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_33, 0, x_32);
lean_ctor_set(x_33, 1, x_31);
x_34 = l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___closed__5;
x_34 = l_Lean_Meta_synthInstance_x3f___lambda__4___closed__4;
x_35 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_35, 0, x_33);
lean_ctor_set(x_35, 1, x_34);
@ -13081,10 +13063,6 @@ l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___closed__2 = _init_l
lean_mark_persistent(l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___closed__2);
l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___closed__3 = _init_l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___closed__3();
lean_mark_persistent(l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___closed__3);
l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___closed__4 = _init_l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___closed__4();
lean_mark_persistent(l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___closed__4);
l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___closed__5 = _init_l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___closed__5();
lean_mark_persistent(l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___closed__5);
l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkCongrArgImp___closed__1 = _init_l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkCongrArgImp___closed__1();
lean_mark_persistent(l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkCongrArgImp___closed__1);
l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkCongrArgImp___closed__2 = _init_l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkCongrArgImp___closed__2();

4330
stage0/stdlib/Lean/Meta/SynthInstance.c generated
View file

File diff suppressed because it is too large Load diff

8
stage0/stdlib/Lean/Meta/Tactic/Replace.c generated
View file

@ -35,7 +35,6 @@ lean_object* l_Lean_Meta_changeLocalDecl___lambda__1___closed__4;
lean_object* l_Lean_Meta_checkNotAssigned___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_replaceLocalDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_changeLocalDecl_match__2(lean_object*);
extern lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___closed__5;
lean_object* l_Lean_mkAppN(lean_object*, lean_object*);
lean_object* l_Lean_Meta_changeLocalDecl___closed__2;
lean_object* l_Lean_Meta_change___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -44,6 +43,7 @@ lean_object* l_Lean_Meta_replaceTargetDefEq___lambda__1(lean_object*, lean_objec
lean_object* l_Lean_Meta_changeLocalDecl___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_change___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_changeLocalDecl___closed__1;
extern lean_object* l_Lean_Meta_synthInstance_x3f___lambda__4___closed__4;
lean_object* l_Lean_Meta_mkAppM___at_Lean_Meta_mkDecideProof___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_replaceTargetEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getMVarType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1132,7 +1132,7 @@ x_16 = l_Lean_Meta_change___lambda__2___closed__2;
x_17 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set(x_17, 1, x_15);
x_18 = l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___closed__5;
x_18 = l_Lean_Meta_synthInstance_x3f___lambda__4___closed__4;
x_19 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_19, 0, x_17);
lean_ctor_set(x_19, 1, x_18);
@ -1559,7 +1559,7 @@ x_72 = l_Lean_Meta_change___lambda__2___closed__2;
x_73 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_73, 0, x_72);
lean_ctor_set(x_73, 1, x_71);
x_74 = l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___closed__5;
x_74 = l_Lean_Meta_synthInstance_x3f___lambda__4___closed__4;
x_75 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_75, 0, x_73);
lean_ctor_set(x_75, 1, x_74);
@ -1893,7 +1893,7 @@ x_153 = l_Lean_Meta_change___lambda__2___closed__2;
x_154 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_154, 0, x_153);
lean_ctor_set(x_154, 1, x_152);
x_155 = l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___closed__5;
x_155 = l_Lean_Meta_synthInstance_x3f___lambda__4___closed__4;
x_156 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_156, 0, x_154);
lean_ctor_set(x_156, 1, x_155);

14
stage0/stdlib/Lean/Parser/Command.c generated
View file

@ -250,6 +250,7 @@ lean_object* l_Lean_Parser_Command_optDeclSig___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_ctor___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_axiom_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Command_structImplicitBinder___elambda__1___closed__6;
extern lean_object* l_Lean_Parser_Term_doForDecl___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_def___elambda__1___closed__8;
lean_object* l_Lean_Parser_Command_attribute_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_declaration_formatter___closed__7;
@ -434,7 +435,6 @@ lean_object* l_Lean_Parser_Command_visibility___closed__1;
lean_object* l_Lean_Parser_Command_universes___closed__2;
lean_object* l_Lean_Parser_Command_exit___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_constant_formatter___closed__7;
extern lean_object* l_Lean_Parser_Term_doFor___closed__1;
lean_object* l_Lean_Parser_Command_declValSimple___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_structFields___elambda__1___closed__22;
lean_object* l_Lean_Parser_Command_end_formatter___closed__1;
@ -1163,6 +1163,7 @@ lean_object* l_Lean_Parser_Command_classInductive_parenthesizer___closed__3;
lean_object* l_Lean_PrettyPrinter_Formatter_toggleInsideQuot_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_637____closed__24;
lean_object* l_Lean_Parser_Command_reduce___elambda__1___closed__2;
extern lean_object* l_Lean_Parser_Term_doForDecl_formatter___closed__2;
extern lean_object* l_Lean_Parser_Attr_externEntry_formatter___closed__2;
lean_object* l_Lean_Parser_Command_section___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_variables___closed__4;
@ -1208,7 +1209,6 @@ lean_object* l_Lean_Parser_Command_section___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_export_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Command_variable_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_optDeriving___elambda__1___closed__11;
extern lean_object* l_Lean_Parser_Term_doFor_formatter___closed__3;
lean_object* l_Lean_Parser_Command_theorem_formatter___closed__2;
lean_object* l_Lean_Parser_Command_classInductive_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Command_inferMod___elambda__1___closed__1;
@ -2255,6 +2255,7 @@ lean_object* l_Lean_Parser_Command_docComment_formatter___closed__1;
lean_object* l_Lean_Parser_Command_partial_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Command_exit___closed__3;
lean_object* l_Lean_Parser_Command_unsafe___elambda__1(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_doForDecl___closed__1;
lean_object* l_Lean_Parser_Command_declModifiers___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_builtin__initialize;
lean_object* l_Lean_Parser_Command_variable___closed__7;
@ -2359,7 +2360,6 @@ lean_object* l_Lean_Parser_Command_open_formatter___closed__4;
lean_object* l_Lean_Parser_Command_def___closed__2;
lean_object* l_Lean_Parser_mkAntiquot(lean_object*, lean_object*, uint8_t);
lean_object* l_Lean_Parser_Command_init__quot___elambda__1___closed__3;
extern lean_object* l_Lean_Parser_Term_doFor___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_ctor___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_optDeclSig___elambda__1___closed__1;
lean_object* l_Lean_Parser_Command_variables___elambda__1(lean_object*, lean_object*);
@ -30319,7 +30319,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Char_quote___closed__1;
x_2 = l_Lean_Parser_Term_doFor___elambda__1___closed__6;
x_2 = l_Lean_Parser_Term_doForDecl___elambda__1___closed__6;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
@ -30357,7 +30357,7 @@ x_8 = lean_ctor_get(x_4, 0);
lean_inc(x_8);
x_9 = lean_array_get_size(x_8);
lean_dec(x_8);
x_10 = l_Lean_Parser_Term_doFor___elambda__1___closed__6;
x_10 = l_Lean_Parser_Term_doForDecl___elambda__1___closed__6;
x_11 = l_Lean_Parser_Command_in___elambda__1___closed__4;
lean_inc(x_1);
x_12 = l_Lean_Parser_symbolFnAux(x_10, x_11, x_1, x_4);
@ -30395,7 +30395,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_quot___closed__1;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Term_doFor___closed__1;
x_3 = l_Lean_Parser_Term_doForDecl___closed__1;
x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
return x_4;
}
@ -30465,7 +30465,7 @@ static lean_object* _init_l_Lean_Parser_Command_in_formatter___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_doFor_formatter___closed__3;
x_1 = l_Lean_Parser_Term_doForDecl_formatter___closed__2;
x_2 = l_Lean_Parser_Term_quot_formatter___closed__2;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);

713
stage0/stdlib/Lean/Parser/Do.c generated
View file

File diff suppressed because it is too large Load diff

4
stage0/stdlib/Lean/PrettyPrinter/Delaborator/Basic.c generated
View file

@ -124,7 +124,6 @@ uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
extern lean_object* l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___lambda__2___closed__4;
lean_object* l_Lean_PrettyPrinter_Delaborator_annotateCurPos(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_Context_pos___default;
extern lean_object* l_Lean_Meta_addPPExplicitToExposeDiff___closed__2;
lean_object* l_Lean_Level_quote___lambda__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Level_LevelToFormat_Result_format___closed__3;
extern lean_object* l_Lean_numLitKind;
@ -224,6 +223,7 @@ lean_object* l_Std_AssocList_find_x3f___at_Lean_PrettyPrinter_Delaborator_delabF
size_t l_USize_land(size_t, size_t);
lean_object* l_Lean_Level_quote___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_failure___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_synthInstance_x3f___lambda__2___closed__4;
lean_object* l_Lean_getPPCoercions___boxed(lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_withAppFn___rarg___closed__4;
lean_object* l_Lean_registerInternalExceptionId(lean_object*, lean_object*);
@ -1471,7 +1471,7 @@ uint8_t l_Lean_getPPAll(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; uint8_t x_4;
x_2 = l_Lean_Meta_addPPExplicitToExposeDiff___closed__2;
x_2 = l_Lean_Meta_synthInstance_x3f___lambda__2___closed__4;
x_3 = 0;
x_4 = l_Lean_KVMap_getBool(x_1, x_2, x_3);
return x_4;