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-03-19 17:04:07 -07:00
parent fdfa3fc0de
commit 1fd70334ab
39 changed files with 73985 additions and 66055 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
stage0/src/Init/Data/Char/Basic.lean
View file

@ -39,10 +39,23 @@ UInt32.decLt _ _
instance decLe (a b : Char) : Decidable (a ≤ b) :=
UInt32.decLe _ _
axiom isValidChar0 : isValidChar 0
abbrev isValidCharNat (n : Nat) : Prop :=
n < 0xd800 ∨ (0xdfff < n ∧ n < 0x110000)
theorem isValidUInt32 (n : Nat) (h : isValidCharNat n) : n < uint32Sz :=
sorry -- TODO: waiting for new frontend
theorem isValidCharOfValidNat (n : Nat) (h : isValidCharNat n) : isValidChar (UInt32.ofNat' n (isValidUInt32 n h)) :=
sorry -- TODO: waiting for new frontend
theorem isValidChar0 : isValidChar 0 :=
sorry -- TODO: waiting for new frontend
@[noinline, matchPattern] def ofNat (n : Nat) : Char :=
if h : isValidChar n.toUInt32 then {val := n.toUInt32, valid := h} else {val := 0, valid := isValidChar0}
if h : isValidCharNat n then
{ val := UInt32.ofNat' n (isValidUInt32 n h), valid := isValidCharOfValidNat n h }
else
{ val := 0, valid := isValidChar0 }
@[inline] def toNat (c : Char) : Nat :=
c.val.toNat

2
stage0/src/Init/Data/UInt.lean
View file

@ -136,6 +136,8 @@ structure UInt32 :=
@[extern "lean_uint32_of_nat"]
def UInt32.ofNat (n : @& Nat) : UInt32 := ⟨Fin.ofNat n⟩
@[extern "lean_uint32_of_nat"]
def UInt32.ofNat' (n : Nat) (h : n < uint32Sz) : UInt32 := ⟨⟨n, h⟩⟩
abbrev Nat.toUInt32 := UInt32.ofNat
@[extern "lean_uint32_to_nat"]
def UInt32.toNat (n : UInt32) : Nat := n.val.val

21
stage0/src/Init/Lean/Elab/Binders.lean
View file

@ -88,24 +88,35 @@ else
else
throwUnsupportedSyntax
private def getBinderIds (ids : Syntax) : TermElabM (Array Syntax) :=
ids.getArgs.mapM $ fun id =>
let k := id.getKind;
if k == identKind || k == `Lean.Parser.Term.hole then
pure id
else if k == `Lean.Parser.Term.id && id.getArgs.size == 2 && (id.getArg 1).isNone then
-- The parser never generates this case, but it is convenient when writting macros.
pure (id.getArg 0)
else
throwError id "identifier or `_` expected"
private def matchBinder (stx : Syntax) : TermElabM (Array BinderView) :=
match stx with
| Syntax.node k args =>
if k == `Lean.Parser.Term.simpleBinder then
if k == `Lean.Parser.Term.simpleBinder then do
-- binderIdent+
let ids := (args.get! 0).getArgs;
ids ← getBinderIds (args.get! 0);
let type := mkHole stx;
ids.mapM $ fun id => do id ← expandBinderIdent id; pure { id := id, type := type, bi := BinderInfo.default }
else if k == `Lean.Parser.Term.explicitBinder then do
-- `(` binderIdent+ binderType (binderDefault <|> binderTactic)? `)`
let ids := (args.get! 1).getArgs;
ids ← getBinderIds (args.get! 1);
let type := expandBinderType (args.get! 2);
let optModifier := args.get! 3;
type ← expandBinderModifier type optModifier;
ids.mapM $ fun id => do id ← expandBinderIdent id; pure { id := id, type := type, bi := BinderInfo.default }
else if k == `Lean.Parser.Term.implicitBinder then
else if k == `Lean.Parser.Term.implicitBinder then do
-- `{` binderIdent+ binderType `}`
let ids := (args.get! 1).getArgs;
ids ← getBinderIds (args.get! 1);
let type := expandBinderType (args.get! 2);
ids.mapM $ fun id => do id ← expandBinderIdent id; pure { id := id, type := type, bi := BinderInfo.implicit }
else if k == `Lean.Parser.Term.instBinder then do

50
stage0/src/Init/Lean/Elab/BuiltinNotation.lean
View file

@ -119,14 +119,18 @@ addDecl ref decl;
compileDecl ref decl;
pure auxName
private def elabClosedTerm (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
e ← elabTermAndSynthesize stx expectedType?;
when e.hasMVar $
throwError stx ("invalid macro application, term contains metavariables" ++ indentExpr e);
when e.hasFVar $
throwError stx ("invalid macro application, term contains free variables" ++ indentExpr e);
pure e
@[builtinTermElab «nativeRefl»] def elabNativeRefl : TermElab :=
fun stx _ => do
let arg := stx.getArg 1;
e ← elabTermAndSynthesize arg none;
when e.hasMVar $
throwError stx ("invalid `nativeRefl!` macro application, term contains metavariables" ++ indentExpr e);
when e.hasFVar $
throwError stx ("invalid `nativeRefl!` macro application, term contains free variables" ++ indentExpr e);
e ← elabClosedTerm arg none;
type ← inferType stx e;
type ← whnf stx type;
unless (type.isConstOf `Bool || type.isConstOf `Nat) $
@ -144,7 +148,41 @@ fun stx _ => do
rflPrf ← liftMetaM stx $ Meta.mkEqRefl val;
let r := mkApp3 (Lean.mkConst reduceThm) aux val rflPrf;
eq ← liftMetaM stx $ Meta.mkEq e val;
pure $ mkApp2 (Lean.mkConst `id [levelZero]) eq r
mkExpectedTypeHint stx r eq
private def getPropToDecide (ref : Syntax) (arg : Syntax) (expectedType? : Option Expr) : TermElabM Expr :=
if arg.isOfKind `Lean.Parser.Term.hole then do
tryPostponeIfNoneOrMVar expectedType?;
match expectedType? with
| none => throwError ref "invalid macro, expected type is not available"
| some expectedType => do
expectedType ← instantiateMVars ref expectedType;
when (expectedType.hasFVar || expectedType.hasMVar) $
throwError ref ("expected type must not contain free or meta variables" ++ indentExpr expectedType);
pure expectedType
else
let prop := mkSort levelZero;
elabClosedTerm arg prop
@[builtinTermElab «nativeDecide»] def elabNativeDecide : TermElab :=
fun stx expectedType? => do
let arg := stx.getArg 1;
p ← getPropToDecide stx arg expectedType?;
d ← mkAppM stx `Decidable.decide #[p];
auxDeclName ← mkNativeReflAuxDecl stx (Lean.mkConst `Bool) d;
rflPrf ← liftMetaM stx $ Meta.mkEqRefl (toExpr true);
let r := mkApp3 (Lean.mkConst `Lean.ofReduceBool) (Lean.mkConst auxDeclName) (toExpr true) rflPrf;
mkExpectedTypeHint stx r p
@[builtinTermElab Lean.Parser.Term.decide] def elabDecide : TermElab :=
fun stx expectedType? => do
let arg := stx.getArg 1;
p ← getPropToDecide stx arg expectedType?;
d ← mkAppM stx `Decidable.decide #[p];
d ← instantiateMVars stx d;
let s := d.appArg!; -- get instance from `d`
rflPrf ← liftMetaM stx $ Meta.mkEqRefl (toExpr true);
pure $ mkApp3 (Lean.mkConst `ofDecideEqTrue) p s rflPrf
def elabInfix (f : Syntax) : Macro :=
fun stx => do

39
stage0/src/Init/Lean/Elab/Term.lean
View file

@ -200,6 +200,15 @@ logInfo ref $
opts ← getOptions;
when (checkTraceOption opts cls) $ logTrace cls ref (msg ())
def logDbgTrace (msg : MessageData) : TermElabM Unit := do
trace `Elab.debug Syntax.missing $ fun _ => msg
/-- For testing `TermElabM` methods. The #eval command will sign the error. -/
def throwErrorIfErrors : TermElabM Unit := do
s ← get;
when s.messages.hasErrors $
throwError Syntax.missing "Error(s)"
@[inline] def traceAtCmdPos (cls : Name) (msg : Unit → MessageData) : TermElabM Unit :=
trace cls Syntax.missing msg
@ -255,6 +264,7 @@ def mkLambda (ref : Syntax) (xs : Array Expr) (e : Expr) : TermElabM Expr := lif
def mkLet (ref : Syntax) (x : Expr) (e : Expr) : TermElabM Expr := mkLambda ref #[x] e
def trySynthInstance (ref : Syntax) (type : Expr) : TermElabM (LOption Expr) := liftMetaM ref $ Meta.trySynthInstance type
def mkAppM (ref : Syntax) (constName : Name) (args : Array Expr) : TermElabM Expr := liftMetaM ref $ Meta.mkAppM constName args
def mkExpectedTypeHint (ref : Syntax) (e : Expr) (expectedType : Expr) : TermElabM Expr := liftMetaM ref $ Meta.mkExpectedTypeHint e expectedType
def decLevel? (ref : Syntax) (u : Level) : TermElabM (Option Level) := liftMetaM ref $ Meta.decLevel? u
def decLevel (ref : Syntax) (u : Level) : TermElabM Level := do
@ -1141,11 +1151,40 @@ fun stx _ =>
| some val => pure $ toExpr val
| none => throwError stx "ill-formed syntax"
instance MetaHasEval {α} [MetaHasEval α] : MetaHasEval (TermElabM α) :=
⟨fun env opts x => do
let ctx : Context := {
config := { opts := opts },
fileName := "<TermElabM>",
fileMap := arbitrary _,
cmdPos := 0,
currNamespace := Name.anonymous,
currRecDepth := 0,
maxRecDepth := getMaxRecDepth opts
};
let showMessages (s : State) : IO Unit := do {
s.messages.forM $ fun m => IO.println $ format m
};
match x ctx { env := env } with
| EStateM.Result.ok a s => do
showMessages s;
MetaHasEval.eval s.env opts a
| EStateM.Result.error (Exception.ex (Elab.Exception.error err)) s => do
showMessages s;
throw (IO.userError (toString (format err)))
| EStateM.Result.error (Exception.ex Elab.Exception.unsupportedSyntax) s => do
showMessages s;
throw (IO.userError "error: unsupported syntax")
| EStateM.Result.error Exception.postpone s => do
showMessages s;
throw (IO.userError "error: elaborator posponed")⟩
end Term
@[init] private def regTraceClasses : IO Unit := do
registerTraceClass `Elab.postpone;
registerTraceClass `Elab.coe;
registerTraceClass `Elab.debug;
pure ()
export Term (TermElabM)

30
stage0/src/Init/Lean/Meta/AppBuilder.lean
View file

@ -3,34 +3,18 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Init.Lean.Util.Recognizers
import Init.Lean.Meta.SynthInstance
namespace Lean
@[inline] def Expr.eq? (p : Expr) : Option (Expr × Expr × Expr) :=
if p.isAppOfArity `Eq 3 then
some (p.getArg! 0, p.getArg! 1, p.getArg! 2)
else
none
@[inline] def Expr.iff? (p : Expr) : Option (Expr × Expr) :=
if p.isAppOfArity `Iff 2 then
some (p.getArg! 0, p.getArg! 1)
else
none
@[inline] def Expr.heq? (p : Expr) : Option (Expr × Expr × Expr × Expr) :=
if p.isAppOfArity `HEq 4 then
some (p.getArg! 0, p.getArg! 1, p.getArg! 2, p.getArg! 4)
else
none
@[inline] def Expr.arrow? : Expr → Option (Expr × Expr)
| Expr.forallE _ α β _ => if β.hasLooseBVars then none else some (α, β)
| _ => none
namespace Meta
/-- Given `e` s.t. `inferType e` is definitionally equal to `expectedType`, return
term `@id expectedType e`. -/
def mkExpectedTypeHint (e : Expr) (expectedType : Expr) : MetaM Expr := do
u ← getLevel expectedType;
pure $ mkApp2 (mkConst `id [u]) expectedType e
def mkEq (a b : Expr) : MetaM Expr := do
aType ← inferType a;
u ← getLevel aType;

6
stage0/src/Init/Lean/Meta/Basic.lean
View file

@ -108,6 +108,7 @@ structure Cache :=
(inferType : PersistentExprStructMap Expr := {})
(funInfo : PersistentHashMap InfoCacheKey FunInfo := {})
(synthInstance : PersistentHashMap Expr (Option Expr) := {})
(whnfDefault : PersistentExprStructMap Expr := {}) -- cache for closed terms and `TransparencyMode.default`
structure Context :=
(config : Config := {})
@ -810,8 +811,9 @@ mctx' ← getMCtx;
modify $ fun s => { mctx := mctx, .. s };
finally x (modify $ fun s => { mctx := mctx', .. s })
@[init] private def regTraceClasses : IO Unit :=
registerTraceClass `Meta
@[init] private def regTraceClasses : IO Unit := do
registerTraceClass `Meta;
registerTraceClass `Meta.debug
def run {α} (env : Environment) (x : MetaM α) (maxRecDepth := 10000) : Except Exception α :=
match x { maxRecDepth := maxRecDepth, currRecDepth := 0 } { env := env } with

15
stage0/src/Init/Lean/Meta/Tactic/Target.lean
View file

@ -16,12 +16,12 @@ namespace Meta
def replaceTargetEq (mvarId : MVarId) (newTarget : Expr) (eqProof : Expr) : MetaM MVarId := do
withMVarContext mvarId $ do
checkNotAssigned mvarId `replaceTarget;
tag ← getMVarTag mvarId;
newMVar ← mkFreshExprSyntheticOpaqueMVar newTarget tag;
target ← getMVarType mvarId;
u ← getLevel target;
eq ← mkEq target newTarget;
let newProof := mkApp2 (mkConst `id [levelZero]) eq eqProof; -- checkpoint for eqProof
tag ← getMVarTag mvarId;
newMVar ← mkFreshExprSyntheticOpaqueMVar newTarget tag;
target ← getMVarType mvarId;
u ← getLevel target;
eq ← mkEq target newTarget;
newProof ← mkExpectedTypeHint eqProof eq;
let newVal := mkAppN (Lean.mkConst `Eq.mpr [u]) #[target, newTarget, eqProof, newMVar];
assignExprMVar mvarId newMVar;
pure newMVar.mvarId!
@ -41,8 +41,7 @@ withMVarContext mvarId $ do
else do
tag ← getMVarTag mvarId;
newMVar ← mkFreshExprSyntheticOpaqueMVar newTarget tag;
u ← getLevel target;
let newVal := mkApp2 (Lean.mkConst `id [u]) target newMVar;
newVal ← mkExpectedTypeHint newMVar target;
assignExprMVar mvarId newMVar;
pure newMVar.mvarId!

49
stage0/src/Init/Lean/Meta/WHNF.lean
View file

@ -85,21 +85,46 @@ else match e with
else pure none
| _ => pure none
@[inline] private def useWHNFCache (e : Expr) : MetaM Bool := do
-- We cache only consed terms
if e.hasFVar then pure false
else do
ctx ← read;
pure $ ctx.config.transparency == TransparencyMode.default
@[inline] private def cached? (useCache : Bool) (e : Expr) : MetaM (Option Expr) := do
if useCache then do
s ← get;
pure $ s.cache.whnfDefault.find? e
else
pure none
private def cache (useCache : Bool) (e r : Expr) : MetaM Expr := do
when useCache $
modify $ fun s => { cache := { whnfDefault := s.cache.whnfDefault.insert e r, .. s.cache }, .. s };
pure r
partial def whnfImpl : Expr → MetaM Expr
| e => Lean.WHNF.whnfEasyCases getLocalDecl getExprMVarAssignment? e $ fun e => do
e ← whnfCore e;
v? ← reduceNat? e;
match v? with
| some v => pure v
| none => do
v? ← reduceNative? e;
useCache ← useWHNFCache e;
e? ← cached? useCache e;
match e? with
| some e' => pure e'
| none => do
e' ← whnfCore e;
v? ← reduceNat? e';
match v? with
| some v => pure v
| none => do
e? ← unfoldDefinition? e;
match e? with
| some e => whnfImpl e
| none => pure e
| some v => cache useCache e v
| none => do
v? ← reduceNative? e';
match v? with
| some v => cache useCache e v
| none => do
e? ← unfoldDefinition? e';
match e? with
| some e => whnfImpl e
| none => cache useCache e e'
@[init] def setWHNFRef : IO Unit :=
whnfRef.set whnfImpl

4
stage0/src/Init/Lean/Parser/Term.lean
View file

@ -210,7 +210,9 @@ def checkIsSort := checkStackTop (fun stx => stx.isOfKind `Lean.Parser.Term.type
@[builtinTermParser] def tacticBlock := parser! symbol "begin " appPrec >> Tactic.seq >> "end"
@[builtinTermParser] def byTactic := parser! symbol "by " leadPrec >> Tactic.nonEmptySeq
-- Use `unboxSingleton` trick similar to the one used at Command.lean for `Term.stxQuot`
@[builtinTermParser] def tacticStxQuot : Parser := node `Lean.Parser.Term.stxQuot $ symbol "`(tactic|" appPrec >> sepBy1 tacticParser "; " true true >> ")"
@[builtinTermParser] def tacticStxQuot : Parser := node `Lean.Parser.Term.stxQuot $ symbol "`(tactic|" appPrec >> sepBy1 tacticParser "; " true true >> ")"
@[builtinTermParser] def levelStxQuot : Parser := node `Lean.Parser.Term.stxQuot $ symbol "`(level|" appPrec >> levelParser >> ")"
@[builtinTermParser] def funBinderStxQuot : Parser := node `Lean.Parser.Term.stxQuot $ symbol "`(funBinder|" appPrec >> funBinder >> ")"
end Term
end Parser

71
stage0/src/Init/Lean/Util/Recognizers.lean Normal file
View file

@ -0,0 +1,71 @@
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Lean.Expr
namespace Lean
namespace Expr
@[inline] def app1? (e : Expr) (fName : Name) : Option Expr :=
if e.isAppOfArity fName 1 then
some $ e.appArg!
else
none
@[inline] def app2? (e : Expr) (fName : Name) : Option (Expr × Expr) :=
if e.isAppOfArity fName 2 then
some $ (e.appFn!.appArg!, e.appArg!)
else
none
@[inline] def app3? (e : Expr) (fName : Name) : Option (Expr × Expr × Expr) :=
if e.isAppOfArity fName 3 then
some $ (e.appFn!.appFn!.appArg!, e.appFn!.appArg!, e.appArg!)
else
none
@[inline] def app4? (e : Expr) (fName : Name) : Option (Expr × Expr × Expr × Expr) :=
if e.isAppOfArity fName 4 then
some $ (e.appFn!.appFn!.appFn!.appArg!, e.appFn!.appFn!.appArg!, e.appFn!.appArg!, e.appArg!)
else
none
@[inline] def eq? (p : Expr) : Option (Expr × Expr × Expr) :=
p.app3? `Eq
@[inline] def iff? (p : Expr) : Option (Expr × Expr) :=
p.app2? `Iff
@[inline] def heq? (p : Expr) : Option (Expr × Expr × Expr × Expr) :=
p.app4? `HEq
@[inline] def arrow? : Expr → Option (Expr × Expr)
| Expr.forallE _ α β _ => if β.hasLooseBVars then none else some (α, β)
| _ => none
partial def listLitAux : Expr → List Expr → Option (List Expr)
| e, acc =>
if e.isAppOfArity `List.nil 1 then
some acc.reverse
else if e.isAppOfArity `List.cons 3 then
listLitAux e.appArg! (e.appFn!.appArg! :: acc)
else
none
def listLit? (e : Expr) : Option (List Expr) :=
listLitAux e []
def arrayLit? (e : Expr) : Option (List Expr) :=
match e.app2? `List.toArray with
| some (_, e) => e.listLit?
| none => none
/-- Recognize `α × β` -/
def prod? (e : Expr) : Option (Expr × Expr) :=
e.app2? `Prod
end Expr
end Lean

2
stage0/src/kernel/inductive.cpp
View file

@ -1126,7 +1126,7 @@ expr nat_lit_to_constructor(expr const & e) {
}
expr string_lit_to_constructor(expr const & e) {
lean_assert(is_str_lit(e));
lean_assert(is_string_lit(e));
string_ref const & s = lit_value(e).get_string();
buffer<unsigned> cs;
utf8_decode(s.to_std_string(), cs);

2
stage0/stdlib/CMakeLists.txt
View file

File diff suppressed because one or more lines are too long

54
stage0/stdlib/Init/Data/Char/Basic.c
View file

@ -20,7 +20,6 @@ uint8_t l_Char_isUpper(uint32_t);
uint8_t l_Char_isDigit(uint32_t);
uint8_t l_Char_isWhitespace(uint32_t);
lean_object* l_Char_toNat___boxed(lean_object*);
uint32_t lean_uint32_of_nat(lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
uint8_t l_Char_lt(uint32_t, uint32_t);
lean_object* l_Char_toNat(uint32_t);
@ -33,6 +32,7 @@ uint8_t l_Char_isLower(uint32_t);
lean_object* l_Char_HasSizeof(uint32_t);
lean_object* l_Char_isAlphanum___boxed(lean_object*);
uint32_t l_Char_Inhabited;
uint32_t lean_uint32_of_nat(lean_object*);
lean_object* l_Char_isWhitespace___boxed(lean_object*);
uint8_t l_Char_isAlpha(uint32_t);
lean_object* l_Char_decLt___boxed(lean_object*, lean_object*);
@ -52,6 +52,7 @@ uint8_t l_UInt32_decLe(uint32_t, uint32_t);
lean_object* lean_uint32_to_nat(uint32_t);
lean_object* l_Char_decLe___boxed(lean_object*, lean_object*);
uint32_t l_Char_ofNat(lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Char_isDigit___boxed(lean_object*);
lean_object* l_Char_HasSizeof(uint32_t x_1) {
_start:
@ -206,41 +207,46 @@ return x_6;
uint32_t l_Char_ofNat(lean_object* x_1) {
_start:
{
uint32_t x_2; uint32_t x_3; uint8_t x_4;
x_2 = lean_uint32_of_nat(x_1);
x_3 = 55296;
x_4 = x_2 < x_3;
if (x_4 == 0)
lean_object* x_2; uint8_t x_3;
x_2 = lean_unsigned_to_nat(55296u);
x_3 = lean_nat_dec_lt(x_1, x_2);
if (x_3 == 0)
{
uint32_t x_5; uint8_t x_6;
x_5 = 57343;
x_6 = x_5 < x_2;
if (x_6 == 0)
lean_object* x_4; uint8_t x_5;
x_4 = lean_unsigned_to_nat(57343u);
x_5 = lean_nat_dec_lt(x_4, x_1);
if (x_5 == 0)
{
uint32_t x_7;
x_7 = 0;
return x_7;
uint32_t x_6;
lean_dec(x_1);
x_6 = 0;
return x_6;
}
else
{
uint32_t x_8; uint8_t x_9;
x_8 = 1114112;
x_9 = x_2 < x_8;
if (x_9 == 0)
lean_object* x_7; uint8_t x_8;
x_7 = lean_unsigned_to_nat(1114112u);
x_8 = lean_nat_dec_lt(x_1, x_7);
if (x_8 == 0)
{
uint32_t x_9;
lean_dec(x_1);
x_9 = 0;
return x_9;
}
else
{
uint32_t x_10;
x_10 = 0;
x_10 = lean_uint32_of_nat(x_1);
return x_10;
}
else
{
return x_2;
}
}
}
else
{
return x_2;
uint32_t x_11;
x_11 = lean_uint32_of_nat(x_1);
return x_11;
}
}
}
@ -249,7 +255,6 @@ _start:
{
uint32_t x_2; lean_object* x_3;
x_2 = l_Char_ofNat(x_1);
lean_dec(x_1);
x_3 = lean_box_uint32(x_2);
return x_3;
}
@ -530,7 +535,6 @@ x_7 = lean_unsigned_to_nat(32u);
x_8 = lean_nat_add(x_2, x_7);
lean_dec(x_2);
x_9 = l_Char_ofNat(x_8);
lean_dec(x_8);
return x_9;
}
}

11
stage0/stdlib/Init/Data/UInt.c
View file

@ -105,6 +105,7 @@ lean_object* l_UInt8_ofNat___boxed(lean_object*);
uint32_t l_UInt32_add(uint32_t, uint32_t);
size_t l_UInt64_toUSize(uint64_t);
uint32_t l_UInt32_div(uint32_t, uint32_t);
lean_object* l_UInt32_ofNat_x27___boxed(lean_object*, lean_object*);
lean_object* l_USize_ofNat___boxed(lean_object*);
lean_object* l_UInt32_HasDiv___closed__1;
lean_object* l_USize_shiftRight___boxed(lean_object*, lean_object*);
@ -173,6 +174,7 @@ lean_object* l_UInt32_div___boxed(lean_object*, lean_object*);
lean_object* l_USize_hasDecidableLt___boxed(lean_object*, lean_object*);
uint64_t l_UInt64_mod(uint64_t, uint64_t);
lean_object* l_UInt16_add___boxed(lean_object*, lean_object*);
uint32_t lean_uint32_of_nat(lean_object*);
uint64_t l_UInt64_mul(uint64_t, uint64_t);
lean_object* l_UInt32_HasMod___closed__1;
size_t l_USize_land(size_t, size_t);
@ -1139,6 +1141,15 @@ x_3 = lean_box_uint32(x_2);
return x_3;
}
}
lean_object* l_UInt32_ofNat_x27___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint32_t x_3; lean_object* x_4;
x_3 = lean_uint32_of_nat(x_1);
x_4 = lean_box_uint32(x_3);
return x_4;
}
}
uint32_t l_Nat_toUInt32(lean_object* x_1) {
_start:
{

5004
stage0/stdlib/Init/Lean/Elab/Binders.c
View file

File diff suppressed because it is too large Load diff

3156
stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c
View file

File diff suppressed because it is too large Load diff

64
stage0/stdlib/Init/Lean/Elab/DoNotation.c
View file

@ -43,6 +43,7 @@ lean_object* l_Lean_Elab_Term_ProcessedDoElem_inhabited___closed__1;
lean_object* l___private_Init_Lean_Elab_DoNotation_9__extractTypeFormerAppArg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_liftMethod___elambda__1___closed__2;
lean_object* l_Lean_Elab_Term_mkLambda(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__2;
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
uint8_t l___private_Init_Lean_Elab_DoNotation_4__hasLiftMethod(lean_object*);
@ -51,6 +52,7 @@ extern lean_object* l___private_Init_Lean_Elab_Term_5__expandCDot___main___close
lean_object* l_Lean_Elab_Term_synthesizeInst(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_DoNotation_3__getDoElems___boxed(lean_object*);
lean_object* l___private_Init_Lean_Elab_DoNotation_11__processDoElemsAux___main___closed__6;
extern lean_object* l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__7;
lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_do___elambda__1___closed__2;
lean_object* l___private_Init_Lean_Elab_DoNotation_5__expandLiftMethodAux___main___closed__3;
@ -75,12 +77,12 @@ lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_throwUnsupportedSyntax___rarg(lean_object*);
lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__5;
lean_object* l___private_Init_Lean_Elab_DoNotation_12__processDoElems(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__6;
extern lean_object* l_Lean_Parser_Term_doId___elambda__1___closed__2;
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_back___at___private_Init_Lean_Elab_DoNotation_10__mkBind___spec__1___boxed(lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__2;
extern lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___elambda__3___closed__2;
extern lean_object* l___private_Init_Lean_Elab_Quotation_11__letBindRhss___main___closed__11;
extern lean_object* l_Lean_Elab_Term_expandCDot_x3f___closed__3;
@ -119,7 +121,6 @@ lean_object* l___private_Init_Lean_Elab_DoNotation_10__mkBind(lean_object*, lean
extern lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__7;
lean_object* lean_environment_main_module(lean_object*);
uint8_t l_Lean_Expr_isMVar(lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__7;
extern lean_object* l_Lean_Elab_Term_elabLetDecl___closed__2;
extern lean_object* l_Lean_Parser_Term_match___elambda__1___closed__2;
lean_object* l_Lean_mkApp(lean_object*, lean_object*);
@ -128,8 +129,8 @@ lean_object* l_Lean_Syntax_getArgs(lean_object*);
lean_object* l___private_Init_Lean_Elab_DoNotation_11__processDoElemsAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getKind(lean_object*);
lean_object* l___private_Init_Lean_Elab_DoNotation_13__regTraceClasses(lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__4;
lean_object* lean_panic_fn(lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__5;
lean_object* l___regBuiltin_Lean_Elab_Term_elabDo(lean_object*);
lean_object* l___private_Init_Lean_Elab_DoNotation_2__extractBind(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabType(lean_object*, lean_object*, lean_object*);
@ -147,7 +148,6 @@ extern lean_object* l_Lean_Expr_Inhabited;
lean_object* lean_array_pop(lean_object*);
lean_object* l___private_Init_Lean_Elab_DoNotation_7__expandDoElemsAux___main(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabDo(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__4;
lean_object* l___private_Init_Lean_Elab_DoNotation_11__processDoElemsAux___main___closed__1;
lean_object* l___private_Init_Lean_Elab_DoNotation_11__processDoElemsAux___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_DoNotation_11__processDoElemsAux___main___closed__2;
@ -2456,12 +2456,12 @@ x_164 = lean_array_push(x_130, x_163);
x_165 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_165, 0, x_132);
lean_ctor_set(x_165, 1, x_164);
x_166 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__2;
x_166 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__2;
x_167 = lean_array_push(x_166, x_165);
x_168 = lean_array_push(x_167, x_152);
x_169 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__4;
x_169 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__4;
x_170 = lean_array_push(x_168, x_169);
x_171 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__7;
x_171 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__7;
x_172 = lean_array_push(x_170, x_171);
x_173 = lean_array_push(x_130, x_117);
x_174 = lean_alloc_ctor(1, 2, 0);
@ -2476,7 +2476,7 @@ x_180 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_180, 0, x_179);
lean_ctor_set(x_180, 1, x_178);
x_181 = lean_array_push(x_130, x_180);
x_182 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__5;
x_182 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__5;
x_183 = lean_array_push(x_181, x_182);
x_184 = l___private_Init_Lean_Elab_DoNotation_7__expandDoElemsAux___main___closed__5;
x_185 = lean_array_push(x_184, x_145);
@ -2544,12 +2544,12 @@ x_217 = lean_array_push(x_130, x_216);
x_218 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_218, 0, x_132);
lean_ctor_set(x_218, 1, x_217);
x_219 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__2;
x_219 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__2;
x_220 = lean_array_push(x_219, x_218);
x_221 = lean_array_push(x_220, x_205);
x_222 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__4;
x_222 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__4;
x_223 = lean_array_push(x_221, x_222);
x_224 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__7;
x_224 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__7;
x_225 = lean_array_push(x_223, x_224);
x_226 = lean_array_push(x_130, x_117);
x_227 = lean_alloc_ctor(1, 2, 0);
@ -2642,12 +2642,12 @@ x_274 = l_Lean_nullKind___closed__2;
x_275 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_275, 0, x_274);
lean_ctor_set(x_275, 1, x_273);
x_276 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__2;
x_276 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__2;
x_277 = lean_array_push(x_276, x_275);
x_278 = lean_array_push(x_277, x_261);
x_279 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__4;
x_279 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__4;
x_280 = lean_array_push(x_278, x_279);
x_281 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__7;
x_281 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__7;
x_282 = lean_array_push(x_280, x_281);
x_283 = lean_array_push(x_259, x_117);
x_284 = lean_alloc_ctor(1, 2, 0);
@ -2662,7 +2662,7 @@ x_290 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_290, 0, x_289);
lean_ctor_set(x_290, 1, x_288);
x_291 = lean_array_push(x_259, x_290);
x_292 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__5;
x_292 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__5;
x_293 = lean_array_push(x_291, x_292);
x_294 = l___private_Init_Lean_Elab_DoNotation_7__expandDoElemsAux___main___closed__5;
x_295 = lean_array_push(x_294, x_252);
@ -2735,12 +2735,12 @@ x_332 = l_Lean_nullKind___closed__2;
x_333 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_333, 0, x_332);
lean_ctor_set(x_333, 1, x_331);
x_334 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__2;
x_334 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__2;
x_335 = lean_array_push(x_334, x_333);
x_336 = lean_array_push(x_335, x_319);
x_337 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__4;
x_337 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__4;
x_338 = lean_array_push(x_336, x_337);
x_339 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__7;
x_339 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__7;
x_340 = lean_array_push(x_338, x_339);
x_341 = lean_array_push(x_317, x_117);
x_342 = lean_alloc_ctor(1, 2, 0);
@ -3149,12 +3149,12 @@ x_545 = lean_array_push(x_511, x_544);
x_546 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_546, 0, x_513);
lean_ctor_set(x_546, 1, x_545);
x_547 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__2;
x_547 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__2;
x_548 = lean_array_push(x_547, x_546);
x_549 = lean_array_push(x_548, x_533);
x_550 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__4;
x_550 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__4;
x_551 = lean_array_push(x_549, x_550);
x_552 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__7;
x_552 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__7;
x_553 = lean_array_push(x_551, x_552);
x_554 = lean_array_push(x_511, x_498);
x_555 = lean_alloc_ctor(1, 2, 0);
@ -3169,7 +3169,7 @@ x_561 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_561, 0, x_560);
lean_ctor_set(x_561, 1, x_559);
x_562 = lean_array_push(x_511, x_561);
x_563 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__5;
x_563 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__5;
x_564 = lean_array_push(x_562, x_563);
x_565 = l___private_Init_Lean_Elab_DoNotation_7__expandDoElemsAux___main___closed__5;
x_566 = lean_array_push(x_565, x_526);
@ -3237,12 +3237,12 @@ x_598 = lean_array_push(x_511, x_597);
x_599 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_599, 0, x_513);
lean_ctor_set(x_599, 1, x_598);
x_600 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__2;
x_600 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__2;
x_601 = lean_array_push(x_600, x_599);
x_602 = lean_array_push(x_601, x_586);
x_603 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__4;
x_603 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__4;
x_604 = lean_array_push(x_602, x_603);
x_605 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__7;
x_605 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__7;
x_606 = lean_array_push(x_604, x_605);
x_607 = lean_array_push(x_511, x_498);
x_608 = lean_alloc_ctor(1, 2, 0);
@ -3335,12 +3335,12 @@ x_655 = l_Lean_nullKind___closed__2;
x_656 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_656, 0, x_655);
lean_ctor_set(x_656, 1, x_654);
x_657 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__2;
x_657 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__2;
x_658 = lean_array_push(x_657, x_656);
x_659 = lean_array_push(x_658, x_642);
x_660 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__4;
x_660 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__4;
x_661 = lean_array_push(x_659, x_660);
x_662 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__7;
x_662 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__7;
x_663 = lean_array_push(x_661, x_662);
x_664 = lean_array_push(x_640, x_498);
x_665 = lean_alloc_ctor(1, 2, 0);
@ -3355,7 +3355,7 @@ x_671 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_671, 0, x_670);
lean_ctor_set(x_671, 1, x_669);
x_672 = lean_array_push(x_640, x_671);
x_673 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__5;
x_673 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__5;
x_674 = lean_array_push(x_672, x_673);
x_675 = l___private_Init_Lean_Elab_DoNotation_7__expandDoElemsAux___main___closed__5;
x_676 = lean_array_push(x_675, x_633);
@ -3428,12 +3428,12 @@ x_713 = l_Lean_nullKind___closed__2;
x_714 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_714, 0, x_713);
lean_ctor_set(x_714, 1, x_712);
x_715 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__2;
x_715 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__2;
x_716 = lean_array_push(x_715, x_714);
x_717 = lean_array_push(x_716, x_700);
x_718 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__4;
x_718 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__4;
x_719 = lean_array_push(x_717, x_718);
x_720 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__7;
x_720 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__7;
x_721 = lean_array_push(x_719, x_720);
x_722 = lean_array_push(x_698, x_498);
x_723 = lean_alloc_ctor(1, 2, 0);

22
stage0/stdlib/Init/Lean/Elab/Quotation.c
View file

@ -131,7 +131,6 @@ lean_object* l_Lean_Elab_Term_Quotation_HeadInfo_Inhabited___closed__2;
lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__23;
extern lean_object* l_Lean_Parser_Term_num___elambda__1___closed__1;
lean_object* l_List_range(lean_object*);
extern lean_object* l_Lean_listToExpr___rarg___closed__8;
lean_object* l___private_Init_Lean_Elab_Quotation_8__explodeHeadPat___lambda__1___closed__2;
lean_object* lean_string_utf8_extract(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(lean_object*);
@ -175,7 +174,6 @@ extern lean_object* l_Nat_HasOfNat___closed__1;
lean_object* l___private_Init_Lean_Elab_Quotation_13__toPreterm___main___closed__5;
lean_object* l_Lean_Elab_Term_Quotation_match__syntax_expand(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Quotation_oldExpandMatchSyntax___closed__1;
extern lean_object* l_Lean_listToExpr___rarg___closed__4;
lean_object* l___private_Init_Lean_Elab_Quotation_11__letBindRhss___main___closed__8;
lean_object* l___private_Init_Lean_Elab_Quotation_1__quoteName___main(lean_object*);
extern lean_object* l_Lean_mkAppStx___closed__8;
@ -237,6 +235,7 @@ lean_object* l___private_Init_Lean_Elab_Quotation_1__quoteName(lean_object*);
lean_object* l___private_Init_Lean_Elab_Quotation_12__exprPlaceholder___closed__1;
extern lean_object* l_Lean_choiceKind___closed__1;
lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_Quotation_match__syntax_expand___spec__1___closed__3;
extern lean_object* l___private_Init_Lean_Elab_Term_15__mkPairsAux___main___closed__4;
lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__25;
lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__17;
lean_object* l_List_mapM___main___at___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___spec__8___closed__8;
@ -354,6 +353,7 @@ lean_object* l_Lean_Parser_getTokenTable(lean_object*);
lean_object* l_Lean_List_hasQuote(lean_object*);
lean_object* l_ReaderT_bind___at_Lean_Elab_Term_monadLog___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Array_append___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Expr_listLitAux___main___closed__4;
lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__2___closed__3;
lean_object* l___private_Init_Lean_Elab_Quotation_11__letBindRhss___main___closed__7;
uint8_t l_Lean_Elab_Term_Quotation_isAntiquot(lean_object*);
@ -395,7 +395,6 @@ lean_object* l___private_Init_Lean_Elab_Quotation_14__oldRunTermElabM___rarg___c
lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__32;
lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__10;
extern lean_object* l_Lean_prodToExpr___rarg___lambda__1___closed__4;
extern lean_object* l_Lean_Parser_Term_str___elambda__1___closed__2;
extern lean_object* l_Lean_Syntax_inhabited;
lean_object* l___private_Init_Lean_Elab_Quotation_2__quoteList___main(lean_object*);
@ -404,6 +403,7 @@ extern lean_object* l_Lean_mkAppStx___closed__5;
lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__44;
extern lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__3;
lean_object* l_Lean_Parser_Error_toString(lean_object*);
extern lean_object* l_Lean_Expr_listLitAux___main___closed__6;
lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__8;
lean_object* l___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___closed__28;
lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__7;
@ -508,6 +508,7 @@ extern lean_object* l_Lean_mkHole___closed__2;
lean_object* l___private_Init_Lean_Elab_Quotation_10__getPatternVarsAux___main___boxed(lean_object*);
extern lean_object* l_Lean_Parser_Term_stxQuot___elambda__1___closed__3;
lean_object* l___private_Init_Lean_Elab_Quotation_8__explodeHeadPat___lambda__1(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Expr_arrayLit_x3f___closed__2;
lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabStxQuot(lean_object*);
lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__7;
lean_object* l_List_foldl___main___at___private_Init_Lean_Elab_Quotation_13__toPreterm___main___spec__5(lean_object*, lean_object*, lean_object*);
@ -520,7 +521,6 @@ lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elab_Quotation_4__
lean_object* l___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___closed__3;
lean_object* l_Lean_mkStxLit(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__24;
extern lean_object* l_Lean_arrayToExpr___rarg___lambda__1___closed__2;
lean_object* l___private_Init_Lean_Elab_Quotation_14__oldRunTermElabM___rarg(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Quotation_11__letBindRhss___main___closed__13;
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
@ -813,7 +813,7 @@ x_7 = lean_apply_1(x_2, x_5);
x_8 = l_Lean_mkAppStx___closed__9;
x_9 = lean_array_push(x_8, x_6);
x_10 = lean_array_push(x_9, x_7);
x_11 = l_Lean_prodToExpr___rarg___lambda__1___closed__4;
x_11 = l___private_Init_Lean_Elab_Term_15__mkPairsAux___main___closed__4;
x_12 = l_Lean_mkCAppStx(x_11, x_10);
return x_12;
}
@ -831,7 +831,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_listToExpr___rarg___closed__4;
x_2 = l_Lean_Expr_listLitAux___main___closed__4;
x_3 = l_Lean_mkCTermIdFrom(x_1, x_2);
return x_3;
}
@ -860,7 +860,7 @@ x_7 = l___private_Init_Lean_Elab_Quotation_2__quoteList___main___rarg(x_1, x_5);
x_8 = l_Lean_mkAppStx___closed__9;
x_9 = lean_array_push(x_8, x_6);
x_10 = lean_array_push(x_9, x_7);
x_11 = l_Lean_listToExpr___rarg___closed__8;
x_11 = l_Lean_Expr_listLitAux___main___closed__6;
x_12 = l_Lean_mkCAppStx(x_11, x_10);
return x_12;
}
@ -915,7 +915,7 @@ x_3 = l_Array_toList___rarg(x_2);
x_4 = l___private_Init_Lean_Elab_Quotation_2__quoteList___main___rarg(x_1, x_3);
x_5 = l_Lean_mkOptionalNode___closed__2;
x_6 = lean_array_push(x_5, x_4);
x_7 = l_Lean_arrayToExpr___rarg___lambda__1___closed__2;
x_7 = l_Lean_Expr_arrayLit_x3f___closed__2;
x_8 = l_Lean_mkCAppStx(x_7, x_6);
return x_8;
}
@ -1974,7 +1974,7 @@ x_11 = l___private_Init_Lean_Elab_Quotation_2__quoteList___main___at___private_I
x_12 = l_Lean_mkAppStx___closed__9;
x_13 = lean_array_push(x_12, x_10);
x_14 = lean_array_push(x_13, x_11);
x_15 = l_Lean_listToExpr___rarg___closed__8;
x_15 = l_Lean_Expr_listLitAux___main___closed__6;
x_16 = l_Lean_mkCAppStx(x_15, x_14);
return x_16;
}
@ -2008,11 +2008,11 @@ x_9 = l___private_Init_Lean_Elab_Quotation_2__quoteList___main___at___private_In
x_10 = l_Lean_mkAppStx___closed__9;
x_11 = lean_array_push(x_10, x_8);
x_12 = lean_array_push(x_11, x_9);
x_13 = l_Lean_prodToExpr___rarg___lambda__1___closed__4;
x_13 = l___private_Init_Lean_Elab_Term_15__mkPairsAux___main___closed__4;
x_14 = l_Lean_mkCAppStx(x_13, x_12);
x_15 = lean_array_push(x_10, x_14);
x_16 = lean_array_push(x_15, x_5);
x_17 = l_Lean_listToExpr___rarg___closed__8;
x_17 = l_Lean_Expr_listLitAux___main___closed__6;
x_18 = l_Lean_mkCAppStx(x_17, x_16);
return x_18;
}

17
stage0/stdlib/Init/Lean/Elab/StructInst.c
View file

@ -40,6 +40,7 @@ lean_object* lean_mk_empty_array_with_capacity(lean_object*);
uint8_t l_AssocList_contains___main___at___private_Init_Lean_Elab_StructInst_12__mkFieldMap___spec__4(lean_object*, lean_object*);
lean_object* l_List_foldlM___main___at___private_Init_Lean_Elab_StructInst_12__mkFieldMap___spec__10___closed__6;
lean_object* l_List_head_x21___at___private_Init_Lean_Elab_StructInst_19__expandStruct___main___spec__5___boxed(lean_object*);
extern lean_object* l_Lean_Meta_mkExpectedTypeHint___closed__1;
lean_object* l_Lean_Elab_Term_mkFreshExprMVar(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_HashMap_toList___rarg(lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_getHierarchyDepth___main___boxed(lean_object*);
@ -162,7 +163,6 @@ lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault___
lean_object* l_AssocList_contains___main___at___private_Init_Lean_Elab_StructInst_12__mkFieldMap___spec__4___boxed(lean_object*, lean_object*);
lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_assignExprMVar(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_mkTermIdFromIdent___closed__1;
lean_object* l_List_foldl___main___at_Lean_Elab_Term_StructInst_DefaultFields_getHierarchyDepth___main___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_List_mapM___main___at___private_Init_Lean_Elab_StructInst_10__expandParentFields___spec__2___closed__6;
lean_object* l_Lean_Elab_Term_getMainModule___rarg(lean_object*);
@ -494,7 +494,6 @@ lean_object* l___private_Init_Lean_Elab_StructInst_19__expandStruct___main(lean_
lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_reduce___main___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_mkDefaultValueAux_x3f___main___closed__1;
lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_step(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_StructInst_ExpandNonAtomicExplicitSource_main___spec__1___closed__2;
lean_object* l___private_Init_Lean_Elab_StructInst_25__elabStructInstAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -21625,16 +21624,6 @@ lean_dec(x_1);
return x_3;
}
}
lean_object* _init_l_Lean_Elab_Term_StructInst_DefaultFields_mkDefaultValueAux_x3f___main___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_mkTermIdFromIdent___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_mkDefaultValueAux_x3f___main(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
@ -21830,7 +21819,7 @@ block_14:
{
lean_object* x_6; lean_object* x_7; uint8_t x_8;
lean_dec(x_5);
x_6 = l_Lean_Elab_Term_StructInst_DefaultFields_mkDefaultValueAux_x3f___main___closed__1;
x_6 = l_Lean_Meta_mkExpectedTypeHint___closed__1;
x_7 = lean_unsigned_to_nat(2u);
x_8 = l_Lean_Expr_isAppOfArity___main(x_2, x_6, x_7);
if (x_8 == 0)
@ -26090,8 +26079,6 @@ l_List_foldlM___main___at___private_Init_Lean_Elab_StructInst_24__elabStruct___m
lean_mark_persistent(l_List_foldlM___main___at___private_Init_Lean_Elab_StructInst_24__elabStruct___main___spec__1___closed__2);
l_List_foldlM___main___at___private_Init_Lean_Elab_StructInst_24__elabStruct___main___spec__1___closed__3 = _init_l_List_foldlM___main___at___private_Init_Lean_Elab_StructInst_24__elabStruct___main___spec__1___closed__3();
lean_mark_persistent(l_List_foldlM___main___at___private_Init_Lean_Elab_StructInst_24__elabStruct___main___spec__1___closed__3);
l_Lean_Elab_Term_StructInst_DefaultFields_mkDefaultValueAux_x3f___main___closed__1 = _init_l_Lean_Elab_Term_StructInst_DefaultFields_mkDefaultValueAux_x3f___main___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_StructInst_DefaultFields_mkDefaultValueAux_x3f___main___closed__1);
l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefaultAux___main___closed__1 = _init_l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefaultAux___main___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefaultAux___main___closed__1);
l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefaultAux___main___closed__2 = _init_l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefaultAux___main___closed__2();

16
stage0/stdlib/Init/Lean/Elab/Syntax.c
View file

@ -133,6 +133,7 @@ lean_object* l_Lean_Elab_Command_elabMacroRulesAux___closed__25;
lean_object* lean_string_utf8_byte_size(lean_object*);
lean_object* l_Lean_mkAtom(lean_object*);
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__20;
extern lean_object* l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__7;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__10;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__32;
lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -225,6 +226,7 @@ extern lean_object* l_Lean_Parser_Command_def___elambda__1___closed__2;
lean_object* l_Lean_Macro_addMacroScope(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Command_declValSimple___elambda__1___closed__2;
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__5;
lean_object* l_Lean_Elab_Command_elabSyntax___closed__25;
extern lean_object* l_Lean_numLitKind___closed__1;
extern lean_object* l_Lean_Parser_Command_def___elambda__1___closed__1;
@ -377,7 +379,6 @@ lean_object* l_Lean_Syntax_setArg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__18;
lean_object* l_Lean_Elab_Command_elabNoKindMacroRulesAux___closed__3;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__3;
extern lean_object* l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__7;
extern lean_object* l_Lean_Parser_Syntax_sepBy1___elambda__1___closed__1;
uint8_t l_Lean_Parser_isParserCategory(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Syntax_5__withoutLeftRec___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -394,6 +395,7 @@ lean_object* l_Lean_Elab_Command_elabMacroRulesAux___closed__7;
lean_object* l_Lean_Syntax_getArgs(lean_object*);
lean_object* l_Lean_Elab_Term_checkLeftRec___closed__3;
lean_object* l_Lean_Syntax_getKind(lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__4;
extern lean_object* l_Lean_Parser_Term_match__syntax___elambda__1___closed__2;
lean_object* l_Lean_Elab_Command_elabMacroRulesAux___closed__24;
lean_object* l_Array_findMAux___main___at_Lean_Elab_Command_elabMacroRulesAux___spec__1(lean_object*, lean_object*, lean_object*);
@ -406,7 +408,6 @@ lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__111;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__97;
lean_object* l_Array_umapMAux___main___at_Lean_Elab_Command_expandMacro___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Syntax_5__withoutLeftRec(lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__5;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__64;
lean_object* l___private_Init_Lean_Elab_Syntax_1__expandOptPrecedence___boxed(lean_object*);
lean_object* l_Lean_Elab_Command_elabSyntax___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -463,7 +464,6 @@ lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__119;
extern lean_object* l_Lean_Parser_Command_macro___elambda__1___closed__1;
lean_object* l___private_Init_Lean_Elab_Syntax_4__withNotFirst___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__29;
extern lean_object* l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__4;
lean_object* l___private_Init_Lean_Elab_Syntax_7__antiquote___main___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabBinders___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_stxQuot___elambda__1___closed__3;
@ -10419,13 +10419,13 @@ x_90 = l_Lean_Elab_Term_expandCDot_x3f___closed__3;
x_91 = lean_array_push(x_89, x_90);
x_92 = l_Lean_Elab_Command_elabMacroRulesAux___closed__17;
x_93 = lean_array_push(x_92, x_85);
x_94 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__4;
x_94 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__4;
x_95 = lean_array_push(x_93, x_94);
x_96 = lean_array_push(x_95, x_42);
x_97 = lean_unsigned_to_nat(0u);
x_98 = l_Array_iterateMAux___main___at_Array_append___spec__1___rarg(x_7, x_7, x_97, x_21);
lean_dec(x_7);
x_99 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__5;
x_99 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__5;
x_100 = lean_array_push(x_98, x_99);
x_101 = l_Lean_Elab_Command_elabMacroRulesAux___closed__23;
lean_inc(x_10);
@ -10644,13 +10644,13 @@ x_222 = l_Lean_Elab_Term_expandCDot_x3f___closed__3;
x_223 = lean_array_push(x_221, x_222);
x_224 = l_Lean_Elab_Command_elabMacroRulesAux___closed__17;
x_225 = lean_array_push(x_224, x_217);
x_226 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__4;
x_226 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__4;
x_227 = lean_array_push(x_225, x_226);
x_228 = lean_array_push(x_227, x_174);
x_229 = lean_unsigned_to_nat(0u);
x_230 = l_Array_iterateMAux___main___at_Array_append___spec__1___rarg(x_7, x_7, x_229, x_153);
lean_dec(x_7);
x_231 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__5;
x_231 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__5;
x_232 = lean_array_push(x_230, x_231);
x_233 = l_Lean_Elab_Command_elabMacroRulesAux___closed__23;
lean_inc(x_10);
@ -13085,7 +13085,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Command_elabNoKindMacroRulesAux___closed__3;
x_2 = l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__7;
x_2 = l___private_Init_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__7;
x_3 = lean_array_push(x_1, x_2);
return x_3;
}

4786
stage0/stdlib/Init/Lean/Elab/Tactic/Basic.c
View file

File diff suppressed because it is too large Load diff

3974
stage0/stdlib/Init/Lean/Elab/Term.c
View file

File diff suppressed because it is too large Load diff

7417
stage0/stdlib/Init/Lean/Meta/AppBuilder.c
View file

File diff suppressed because it is too large Load diff

56220
stage0/stdlib/Init/Lean/Meta/Basic.c
View file

File diff suppressed because it is too large Load diff

23522
stage0/stdlib/Init/Lean/Meta/ExprDefEq.c
View file

File diff suppressed because it is too large Load diff

11150
stage0/stdlib/Init/Lean/Meta/FunInfo.c
View file

File diff suppressed because it is too large Load diff

1583
stage0/stdlib/Init/Lean/Meta/InferType.c
View file

File diff suppressed because it is too large Load diff

3561
stage0/stdlib/Init/Lean/Meta/SynthInstance.c
View file

File diff suppressed because it is too large Load diff

2033
stage0/stdlib/Init/Lean/Meta/Tactic/Cases.c
View file

File diff suppressed because it is too large Load diff

1718
stage0/stdlib/Init/Lean/Meta/Tactic/Injection.c
View file

File diff suppressed because it is too large Load diff

6768
stage0/stdlib/Init/Lean/Meta/Tactic/Intro.c
View file

File diff suppressed because it is too large Load diff

2866
stage0/stdlib/Init/Lean/Meta/Tactic/Rewrite.c
View file

File diff suppressed because it is too large Load diff

1449
stage0/stdlib/Init/Lean/Meta/Tactic/Subst.c
View file

File diff suppressed because it is too large Load diff

289
stage0/stdlib/Init/Lean/Meta/Tactic/Target.c
View file

@ -26,7 +26,7 @@ lean_object* l_Lean_Meta_getMVarType(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_replaceTargetDefEq___closed__1;
lean_object* l_Lean_Meta_replaceTargetDefEq___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Meta_replaceTargetEq___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_replaceTargetEq___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_assignExprMVar(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_replaceTargetEq___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_expr_eqv(lean_object*, lean_object*);
@ -34,134 +34,119 @@ lean_object* l_Lean_Meta_mkFreshExprMVar(lean_object*, lean_object*, uint8_t, le
lean_object* l_Lean_Meta_replaceTargetDefEq___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getLevel(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getMVarDecl(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_replaceTargetEq___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_replaceTargetEq___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_replaceTargetEq___closed__1;
lean_object* l_Lean_Meta_mkExpectedTypeHint(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_replaceTargetEq___closed__2;
lean_object* l_Lean_Meta_mkEq(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_replaceTargetEq___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
lean_object* l_Lean_Meta_replaceTargetEq___lambda__1(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:
{
lean_object* x_6;
lean_object* x_7;
lean_inc(x_1);
x_6 = l_Lean_Meta_getMVarTag(x_1, x_4, x_5);
if (lean_obj_tag(x_6) == 0)
x_7 = l_Lean_Meta_getMVarTag(x_1, x_5, x_6);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_7; lean_object* x_8; uint8_t x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_7 = lean_ctor_get(x_6, 0);
lean_inc(x_7);
x_8 = lean_ctor_get(x_6, 1);
lean_object* x_8; lean_object* x_9; uint8_t x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_8 = lean_ctor_get(x_7, 0);
lean_inc(x_8);
lean_dec(x_6);
x_9 = 2;
lean_inc(x_4);
x_9 = lean_ctor_get(x_7, 1);
lean_inc(x_9);
lean_dec(x_7);
x_10 = 2;
lean_inc(x_5);
lean_inc(x_2);
x_10 = l_Lean_Meta_mkFreshExprMVar(x_2, x_7, x_9, x_4, x_8);
x_11 = lean_ctor_get(x_10, 0);
lean_inc(x_11);
x_12 = lean_ctor_get(x_10, 1);
x_11 = l_Lean_Meta_mkFreshExprMVar(x_2, x_8, x_10, x_5, x_9);
x_12 = lean_ctor_get(x_11, 0);
lean_inc(x_12);
lean_dec(x_10);
x_13 = lean_ctor_get(x_11, 1);
lean_inc(x_13);
lean_dec(x_11);
lean_inc(x_1);
x_13 = l_Lean_Meta_getMVarType(x_1, x_4, x_12);
if (lean_obj_tag(x_13) == 0)
x_14 = l_Lean_Meta_getMVarType(x_1, x_5, x_13);
if (lean_obj_tag(x_14) == 0)
{
lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_14 = lean_ctor_get(x_13, 0);
lean_inc(x_14);
x_15 = lean_ctor_get(x_13, 1);
lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
lean_dec(x_13);
lean_inc(x_4);
lean_inc(x_14);
x_16 = l_Lean_Meta_getLevel(x_14, x_4, x_15);
if (lean_obj_tag(x_16) == 0)
x_16 = lean_ctor_get(x_14, 1);
lean_inc(x_16);
lean_dec(x_14);
lean_inc(x_5);
lean_inc(x_15);
x_17 = l_Lean_Meta_getLevel(x_15, x_5, x_16);
if (lean_obj_tag(x_17) == 0)
{
lean_object* x_17; lean_object* x_18;
x_17 = lean_ctor_get(x_16, 1);
lean_inc(x_17);
lean_dec(x_16);
lean_inc(x_4);
x_18 = l_Lean_Meta_mkEq(x_14, x_2, x_4, x_17);
if (lean_obj_tag(x_18) == 0)
lean_object* x_18; lean_object* x_19;
x_18 = lean_ctor_get(x_17, 1);
lean_inc(x_18);
lean_dec(x_17);
lean_inc(x_5);
x_19 = l_Lean_Meta_mkEq(x_15, x_2, x_5, x_18);
if (lean_obj_tag(x_19) == 0)
{
lean_object* x_19; lean_object* x_20;
x_19 = lean_ctor_get(x_18, 1);
lean_inc(x_19);
lean_dec(x_18);
lean_inc(x_11);
x_20 = l_Lean_Meta_assignExprMVar(x_1, x_11, x_4, x_19);
lean_dec(x_4);
if (lean_obj_tag(x_20) == 0)
lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_20 = lean_ctor_get(x_19, 0);
lean_inc(x_20);
x_21 = lean_ctor_get(x_19, 1);
lean_inc(x_21);
lean_dec(x_19);
lean_inc(x_5);
x_22 = l_Lean_Meta_mkExpectedTypeHint(x_3, x_20, x_5, x_21);
if (lean_obj_tag(x_22) == 0)
{
uint8_t x_21;
x_21 = !lean_is_exclusive(x_20);
if (x_21 == 0)
{
lean_object* x_22; lean_object* x_23;
x_22 = lean_ctor_get(x_20, 0);
lean_object* x_23; lean_object* x_24;
x_23 = lean_ctor_get(x_22, 1);
lean_inc(x_23);
lean_dec(x_22);
x_23 = l_Lean_Expr_mvarId_x21(x_11);
lean_dec(x_11);
lean_ctor_set(x_20, 0, x_23);
return x_20;
}
else
lean_inc(x_12);
x_24 = l_Lean_Meta_assignExprMVar(x_1, x_12, x_5, x_23);
lean_dec(x_5);
if (lean_obj_tag(x_24) == 0)
{
lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_24 = lean_ctor_get(x_20, 1);
lean_inc(x_24);
lean_dec(x_20);
x_25 = l_Lean_Expr_mvarId_x21(x_11);
lean_dec(x_11);
x_26 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_26, 0, x_25);
lean_ctor_set(x_26, 1, x_24);
return x_26;
}
}
else
uint8_t x_25;
x_25 = !lean_is_exclusive(x_24);
if (x_25 == 0)
{
uint8_t x_27;
lean_dec(x_11);
x_27 = !lean_is_exclusive(x_20);
if (x_27 == 0)
{
return x_20;
lean_object* x_26; lean_object* x_27;
x_26 = lean_ctor_get(x_24, 0);
lean_dec(x_26);
x_27 = l_Lean_Expr_mvarId_x21(x_12);
lean_dec(x_12);
lean_ctor_set(x_24, 0, x_27);
return x_24;
}
else
{
lean_object* x_28; lean_object* x_29; lean_object* x_30;
x_28 = lean_ctor_get(x_20, 0);
x_29 = lean_ctor_get(x_20, 1);
lean_inc(x_29);
x_28 = lean_ctor_get(x_24, 1);
lean_inc(x_28);
lean_dec(x_20);
x_30 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_30, 0, x_28);
lean_ctor_set(x_30, 1, x_29);
lean_dec(x_24);
x_29 = l_Lean_Expr_mvarId_x21(x_12);
lean_dec(x_12);
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_11);
lean_dec(x_4);
lean_dec(x_1);
x_31 = !lean_is_exclusive(x_18);
lean_dec(x_12);
x_31 = !lean_is_exclusive(x_24);
if (x_31 == 0)
{
return x_18;
return x_24;
}
else
{
lean_object* x_32; lean_object* x_33; lean_object* x_34;
x_32 = lean_ctor_get(x_18, 0);
x_33 = lean_ctor_get(x_18, 1);
x_32 = lean_ctor_get(x_24, 0);
x_33 = lean_ctor_get(x_24, 1);
lean_inc(x_33);
lean_inc(x_32);
lean_dec(x_18);
lean_dec(x_24);
x_34 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_34, 0, x_32);
lean_ctor_set(x_34, 1, x_33);
@ -172,24 +157,22 @@ return x_34;
else
{
uint8_t x_35;
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_12);
lean_dec(x_5);
lean_dec(x_1);
x_35 = !lean_is_exclusive(x_16);
x_35 = !lean_is_exclusive(x_22);
if (x_35 == 0)
{
return x_16;
return x_22;
}
else
{
lean_object* x_36; lean_object* x_37; lean_object* x_38;
x_36 = lean_ctor_get(x_16, 0);
x_37 = lean_ctor_get(x_16, 1);
x_36 = lean_ctor_get(x_22, 0);
x_37 = lean_ctor_get(x_22, 1);
lean_inc(x_37);
lean_inc(x_36);
lean_dec(x_16);
lean_dec(x_22);
x_38 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_38, 0, x_36);
lean_ctor_set(x_38, 1, x_37);
@ -200,23 +183,23 @@ return x_38;
else
{
uint8_t x_39;
lean_dec(x_11);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_12);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_1);
x_39 = !lean_is_exclusive(x_13);
x_39 = !lean_is_exclusive(x_19);
if (x_39 == 0)
{
return x_13;
return x_19;
}
else
{
lean_object* x_40; lean_object* x_41; lean_object* x_42;
x_40 = lean_ctor_get(x_13, 0);
x_41 = lean_ctor_get(x_13, 1);
x_40 = lean_ctor_get(x_19, 0);
x_41 = lean_ctor_get(x_19, 1);
lean_inc(x_41);
lean_inc(x_40);
lean_dec(x_13);
lean_dec(x_19);
x_42 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_42, 0, x_40);
lean_ctor_set(x_42, 1, x_41);
@ -227,22 +210,25 @@ return x_42;
else
{
uint8_t x_43;
lean_dec(x_4);
lean_dec(x_15);
lean_dec(x_12);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_43 = !lean_is_exclusive(x_6);
x_43 = !lean_is_exclusive(x_17);
if (x_43 == 0)
{
return x_6;
return x_17;
}
else
{
lean_object* x_44; lean_object* x_45; lean_object* x_46;
x_44 = lean_ctor_get(x_6, 0);
x_45 = lean_ctor_get(x_6, 1);
x_44 = lean_ctor_get(x_17, 0);
x_45 = lean_ctor_get(x_17, 1);
lean_inc(x_45);
lean_inc(x_44);
lean_dec(x_6);
lean_dec(x_17);
x_46 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_46, 0, x_44);
lean_ctor_set(x_46, 1, x_45);
@ -250,6 +236,61 @@ return x_46;
}
}
}
else
{
uint8_t x_47;
lean_dec(x_12);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_47 = !lean_is_exclusive(x_14);
if (x_47 == 0)
{
return x_14;
}
else
{
lean_object* x_48; lean_object* x_49; lean_object* x_50;
x_48 = lean_ctor_get(x_14, 0);
x_49 = lean_ctor_get(x_14, 1);
lean_inc(x_49);
lean_inc(x_48);
lean_dec(x_14);
x_50 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_50, 0, x_48);
lean_ctor_set(x_50, 1, x_49);
return x_50;
}
}
}
else
{
uint8_t x_51;
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_51 = !lean_is_exclusive(x_7);
if (x_51 == 0)
{
return x_7;
}
else
{
lean_object* x_52; lean_object* x_53; lean_object* x_54;
x_52 = lean_ctor_get(x_7, 0);
x_53 = lean_ctor_get(x_7, 1);
lean_inc(x_53);
lean_inc(x_52);
lean_dec(x_7);
x_54 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_54, 0, x_52);
lean_ctor_set(x_54, 1, x_53);
return x_54;
}
}
}
}
lean_object* _init_l_Lean_Meta_replaceTargetEq___closed__1() {
_start:
@ -279,9 +320,10 @@ x_7 = lean_alloc_closure((void*)(l_Lean_Meta_checkNotAssigned___boxed), 4, 2);
lean_closure_set(x_7, 0, x_1);
lean_closure_set(x_7, 1, x_6);
lean_inc(x_1);
x_8 = lean_alloc_closure((void*)(l_Lean_Meta_replaceTargetEq___lambda__1___boxed), 5, 2);
x_8 = lean_alloc_closure((void*)(l_Lean_Meta_replaceTargetEq___lambda__1___boxed), 6, 3);
lean_closure_set(x_8, 0, x_1);
lean_closure_set(x_8, 1, x_2);
lean_closure_set(x_8, 2, x_3);
x_9 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Meta_isClassExpensive___main___spec__4___rarg), 4, 2);
lean_closure_set(x_9, 0, x_7);
lean_closure_set(x_9, 1, x_8);
@ -327,13 +369,13 @@ return x_19;
}
}
}
lean_object* l_Lean_Meta_replaceTargetEq___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
lean_object* l_Lean_Meta_replaceTargetEq___lambda__1___boxed(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:
{
lean_object* x_6;
x_6 = l_Lean_Meta_replaceTargetEq___lambda__1(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_3);
return x_6;
lean_object* x_7;
x_7 = l_Lean_Meta_replaceTargetEq___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_4);
return x_7;
}
}
lean_object* l_Lean_Meta_replaceTargetEq___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
@ -342,7 +384,6 @@ _start:
lean_object* x_6;
x_6 = l_Lean_Meta_replaceTargetEq(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_4);
lean_dec(x_3);
return x_6;
}
}
@ -385,7 +426,8 @@ x_17 = lean_ctor_get(x_15, 1);
lean_inc(x_17);
lean_dec(x_15);
lean_inc(x_4);
x_18 = l_Lean_Meta_getLevel(x_8, x_4, x_17);
lean_inc(x_16);
x_18 = l_Lean_Meta_mkExpectedTypeHint(x_16, x_8, x_4, x_17);
if (lean_obj_tag(x_18) == 0)
{
lean_object* x_19; lean_object* x_20;
@ -540,7 +582,8 @@ x_48 = lean_ctor_get(x_46, 1);
lean_inc(x_48);
lean_dec(x_46);
lean_inc(x_4);
x_49 = l_Lean_Meta_getLevel(x_39, x_4, x_48);
lean_inc(x_47);
x_49 = l_Lean_Meta_mkExpectedTypeHint(x_47, x_39, x_4, x_48);
if (lean_obj_tag(x_49) == 0)
{
lean_object* x_50; lean_object* x_51;

2587
stage0/stdlib/Init/Lean/Meta/WHNF.c
View file

File diff suppressed because it is too large Load diff

704
stage0/stdlib/Init/Lean/Parser/Term.c
View file

@ -109,6 +109,7 @@ lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_
lean_object* l_Lean_Parser_Term_explicit___closed__2;
lean_object* l___regBuiltinParser_Lean_Parser_Term_ge(lean_object*);
lean_object* l_Lean_Parser_Term_nomatch___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_doPat___closed__3;
lean_object* l_Lean_Parser_Term_matchAlt___closed__3;
lean_object* l_Lean_Parser_Term_inaccessible___closed__2;
@ -154,6 +155,7 @@ lean_object* l_Lean_Parser_Term_str___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_andthen___closed__3;
lean_object* l_Lean_Parser_Term_not___elambda__1___closed__7;
lean_object* l_Lean_Parser_Term_checkIsSort___elambda__1___boxed(lean_object*);
lean_object* l_Lean_Parser_Term_funBinderStxQuot___closed__1;
lean_object* l_Lean_Parser_Tactic_seq___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_structInst___closed__6;
lean_object* l___regBuiltinParser_Lean_Parser_Term_explicit(lean_object*);
@ -162,6 +164,7 @@ lean_object* l_Lean_Parser_Term_type___closed__3;
lean_object* l_Lean_Parser_Term_subtype___closed__6;
lean_object* l___regBuiltinParser_Lean_Parser_Term_append(lean_object*);
lean_object* l_Lean_Parser_Term_nomatch___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_levelStxQuot___closed__5;
lean_object* l_Lean_Parser_darrow___elambda__1___closed__8;
lean_object* l_Lean_Parser_Term_haveAssign___closed__2;
lean_object* l_Lean_Parser_Term_nativeDecide___elambda__1___closed__1;
@ -186,6 +189,7 @@ lean_object* l_Lean_Parser_Term_instBinder___closed__5;
lean_object* l_Lean_Parser_Term_inaccessible___elambda__1___closed__7;
lean_object* l_Lean_Parser_Term_seqLeft___closed__2;
lean_object* l_Lean_Parser_Term_namedArgument___closed__5;
lean_object* l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__5;
lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_matchAlts___elambda__1___spec__18___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_seq;
lean_object* l_Lean_Parser_Term_show___elambda__1___closed__8;
@ -233,6 +237,7 @@ lean_object* l_Lean_Parser_Term_div___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_if___closed__10;
lean_object* l_Lean_Parser_Term_namedPattern___elambda__1___closed__6;
lean_object* l_Lean_Parser_Term_subst___closed__4;
lean_object* l___regBuiltinParser_Lean_Parser_Term_levelStxQuot___closed__1;
lean_object* l_Lean_Parser_Term_prop;
lean_object* l_Lean_Parser_Term_binderTactic___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__2;
@ -256,9 +261,11 @@ lean_object* l_Lean_Parser_Term_where___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_letPatDecl;
lean_object* l_Lean_Parser_Term_sortApp___closed__4;
lean_object* l_Lean_Parser_Term_bnot___closed__2;
lean_object* l___regBuiltinParser_Lean_Parser_Term_levelStxQuot(lean_object*);
lean_object* l_Lean_Parser_Term_typeAscription___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_band___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_funBinderStxQuot___closed__2;
lean_object* l_Lean_Parser_Term_explicitBinder___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_and___closed__3;
lean_object* l_Lean_Parser_Term_tupleTail___elambda__1___closed__1;
@ -446,6 +453,7 @@ lean_object* l_Lean_Parser_Term_instBinder___closed__3;
lean_object* l_Lean_Parser_Term_nativeRefl___elambda__1___closed__6;
lean_object* l_Lean_Parser_Term_and;
lean_object* l_Lean_Parser_Term_gt___elambda__1(lean_object*, lean_object*);
lean_object* l___regBuiltinParser_Lean_Parser_Term_levelStxQuot___closed__2;
lean_object* l_Lean_Parser_Term_bracketedDoSeq___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_suffices___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_parenSpecial___closed__1;
@ -471,6 +479,7 @@ lean_object* l_Lean_Parser_Term_bracktedBinder___elambda__1(lean_object*, lean_o
lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__13;
lean_object* l_Lean_Parser_Term_anonymousCtor___closed__9;
lean_object* l_Lean_Parser_Term_sorry___closed__1;
lean_object* l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_let_x21___closed__6;
lean_object* l_Lean_Parser_Term_ge___elambda__1___closed__4;
@ -525,6 +534,7 @@ lean_object* l_Lean_Parser_Term_uminus___closed__7;
lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_matchAlts___elambda__1___spec__2___closed__4;
lean_object* l_Lean_Parser_Term_suffices___elambda__1___closed__7;
lean_object* l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__8;
lean_object* l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_borrowed;
lean_object* l_Lean_Parser_Term_and___closed__1;
lean_object* l_Lean_Parser_Term_paren___closed__7;
@ -579,12 +589,14 @@ lean_object* l_Lean_Parser_Term_str;
lean_object* l_Lean_Parser_Term_decide___closed__5;
lean_object* l_Lean_Parser_Term_structInstLVal___closed__5;
lean_object* l_Lean_Parser_Term_binderTactic___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_depArrow___closed__8;
lean_object* l_Lean_Parser_Term_dollarProj___elambda__1___closed__3;
lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_nativeDecide___elambda__1___closed__6;
lean_object* l___regBuiltinParser_Lean_Parser_Term_sorry(lean_object*);
lean_object* l_Lean_Parser_Term_nomatch___closed__4;
lean_object* l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_or___elambda__1___closed__2;
lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__3;
lean_object* l_Lean_Parser_Term_listLit___elambda__1(lean_object*, lean_object*);
@ -640,6 +652,7 @@ lean_object* l_Lean_Parser_Term_num___closed__2;
lean_object* l_Lean_Parser_Term_typeAscription___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_binderDefault;
lean_object* l_Lean_Parser_Term_namedPattern___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__9;
lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_matchAlts___elambda__1___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_uminus___elambda__1___closed__1;
@ -829,6 +842,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Term_dollar(lean_object*);
lean_object* l_Lean_Parser_Term_explicitUniv___closed__5;
lean_object* l_Lean_Parser_Term_let___closed__6;
lean_object* l_Lean_Parser_Term_byTactic___elambda__1___closed__6;
lean_object* l_Lean_Parser_Term_funBinderStxQuot___closed__6;
lean_object* l_Lean_Parser_Term_lt___closed__2;
lean_object* l_Lean_Parser_Term_sorry___closed__3;
lean_object* l_Lean_Parser_Term_instBinder___elambda__1___closed__2;
@ -873,6 +887,7 @@ lean_object* l_Lean_Parser_Term_bnot___closed__5;
lean_object* l_Lean_Parser_Term_structInstField___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_paren___closed__4;
uint8_t l_Lean_Parser_tryAnti(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_funBinderStxQuot;
lean_object* l_Lean_Parser_Term_mul;
lean_object* l_Lean_Parser_Term_ge___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_quotedName;
@ -912,6 +927,7 @@ lean_object* l_Lean_Parser_Term_explicitUniv___closed__3;
lean_object* l___regBuiltinParser_Lean_Parser_Term_bne(lean_object*);
lean_object* l___regBuiltinParser_Lean_Parser_Term_inaccessible(lean_object*);
lean_object* l_Lean_Parser_Term_depArrow___closed__2;
lean_object* l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_structInst___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__13;
lean_object* l_Lean_Parser_Term_andM___closed__1;
@ -1210,6 +1226,7 @@ lean_object* l_Lean_Parser_Term_sorry___elambda__1___closed__6;
lean_object* l_Lean_Parser_Term_haveAssign___elambda__1___closed__8;
lean_object* l_Lean_Parser_Term_num___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_and___closed__2;
lean_object* l___regBuiltinParser_Lean_Parser_Term_funBinderStxQuot(lean_object*);
lean_object* l_Lean_Parser_Term_prop___closed__4;
lean_object* l___regBuiltinParser_Lean_Parser_Term_mul(lean_object*);
lean_object* l_Lean_Parser_Term_leftArrow___elambda__1___closed__8;
@ -1221,6 +1238,7 @@ lean_object* l_Lean_Parser_Term_binderType___elambda__2(lean_object*, lean_objec
lean_object* l_Lean_Parser_Term_bracketedDoSeq___closed__2;
lean_object* l_Lean_Parser_Term_andthen;
lean_object* l_Lean_Parser_Term_matchAlt___closed__11;
lean_object* l_Lean_Parser_Term_levelStxQuot___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_or___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_mapConst___closed__3;
lean_object* l_Lean_Parser_Term_doPat___closed__9;
@ -1263,6 +1281,7 @@ lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_matchAlts___elambda__1
lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_matchAlts___elambda__1___spec__16(lean_object*, lean_object*, uint8_t, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_borrowed___elambda__1___closed__9;
lean_object* l_Lean_Parser_Term_typeAscription___closed__3;
extern lean_object* l_Lean_Parser_Level_paren___closed__4;
lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_matchAlts___elambda__1___spec__2___closed__5;
lean_object* l_Lean_Parser_Term_have___closed__10;
lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__15;
@ -1474,6 +1493,7 @@ lean_object* l_Lean_Parser_Term_structInstLVal___closed__4;
lean_object* l_Lean_Parser_Term_matchAlt;
lean_object* l_Lean_Parser_Term_or___closed__3;
lean_object* l_Lean_Parser_Term_inaccessible___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_funBinderStxQuot___closed__4;
lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_subst___elambda__1___spec__1(uint8_t, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_binderDefault___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_nomatch___closed__2;
@ -1664,6 +1684,7 @@ lean_object* l_Lean_Parser_Term_subtype___closed__10;
lean_object* l_Lean_Parser_Term_append___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_tupleTail___closed__2;
lean_object* l_Lean_Parser_Term_structInstLVal___closed__11;
lean_object* l_Lean_Parser_Term_levelStxQuot___closed__1;
lean_object* l_Lean_Parser_Term_dollar___closed__4;
lean_object* l___regBuiltinParser_Lean_Parser_Term_decide(lean_object*);
lean_object* l_Lean_Parser_Term_arrayRef___closed__1;
@ -1672,6 +1693,7 @@ lean_object* l_Lean_Parser_Term_nativeRefl___elambda__1___closed__1;
lean_object* l_Lean_Parser_dollarSymbol___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_mapConst___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_map___closed__2;
lean_object* l_Lean_Parser_Term_funBinderStxQuot___closed__5;
lean_object* l_Lean_Parser_Term_or;
lean_object* l_Lean_Parser_Term_orM___elambda__1(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_unicodeSymbolFn___closed__1;
@ -1691,12 +1713,14 @@ lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_structInstField___closed__5;
lean_object* l_Lean_Parser_Term_matchAlts___closed__2;
lean_object* l_Lean_Parser_Term_doPat___elambda__1___closed__6;
lean_object* l___regBuiltinParser_Lean_Parser_Term_funBinderStxQuot___closed__1;
lean_object* l_Lean_Parser_Term_append;
lean_object* l_Lean_Parser_Term_letIdLhs___closed__6;
lean_object* l_Lean_Parser_Term_borrowed___elambda__1___closed__2;
lean_object* l_Lean_Parser_Tactic_seq___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_not___closed__1;
lean_object* l_Lean_Parser_Term_uminus___closed__1;
lean_object* l_Lean_Parser_Term_funBinderStxQuot___closed__3;
lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2(uint8_t, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_map___closed__1;
lean_object* l_Lean_Parser_Term_doLet___elambda__1___closed__1;
@ -1710,6 +1734,7 @@ lean_object* l_Lean_Parser_Term_gt;
lean_object* l_Lean_Parser_Term_doExpr___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_tparser_x21___closed__2;
lean_object* l_Lean_Parser_Term_matchAlts___boxed(lean_object*);
lean_object* l_Lean_Parser_Term_levelStxQuot___closed__3;
lean_object* l_Lean_Parser_Term_not___closed__4;
lean_object* l_Lean_Parser_Term_subst___closed__1;
lean_object* l_Lean_Parser_Term_beq___elambda__1___closed__3;
@ -1824,6 +1849,7 @@ lean_object* l_Lean_Parser_Term_inaccessible___elambda__1___closed__6;
lean_object* l_Lean_Parser_Tactic_seq___closed__1;
lean_object* l_Lean_Parser_nameLit___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_tacticBlock___closed__6;
lean_object* l_Lean_Parser_Term_levelStxQuot;
lean_object* l_Lean_Parser_Term_equiv___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_letPatDecl___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_letIdDecl___closed__8;
@ -1861,6 +1887,7 @@ lean_object* l_Lean_Parser_Term_match__syntax___elambda__1___closed__7;
lean_object* l___regBuiltinParser_Lean_Parser_Term_arrow(lean_object*);
lean_object* l_Lean_Parser_Term_modN___closed__3;
lean_object* l___regBuiltinParser_Lean_Parser_Term_sortApp(lean_object*);
lean_object* l_Lean_Parser_Term_levelStxQuot___closed__4;
lean_object* l_Lean_Parser_Term_typeAscription___closed__6;
lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_explicitUniv___elambda__1___spec__2___closed__3;
lean_object* l_Lean_Parser_Term_lt;
@ -1880,6 +1907,7 @@ lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__12;
lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_explicitUniv___elambda__1___spec__1(uint8_t, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_seqRight___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_funBinder___closed__4;
lean_object* l___regBuiltinParser_Lean_Parser_Term_funBinderStxQuot___closed__2;
lean_object* l___regBuiltinParser_Lean_Parser_Term_match(lean_object*);
lean_object* l___regBuiltinParser_Lean_Parser_Term_depArrow(lean_object*);
lean_object* l_Lean_Parser_Term_simpleBinder___elambda__1___closed__3;
@ -1938,6 +1966,7 @@ lean_object* l_Lean_Parser_regBuiltinTacticParserAttr___closed__4;
lean_object* l_Lean_Parser_Term_mapConstRev___closed__2;
lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__7;
lean_object* l_Lean_Parser_Term_tupleTail___closed__4;
lean_object* l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_nativeRefl___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_orelse___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_gt___closed__3;
@ -1992,6 +2021,7 @@ lean_object* l_Lean_Parser_Term_binderIdent___elambda__1(lean_object*, lean_obje
lean_object* l_Lean_Parser_Term_char___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_borrowed___elambda__1___closed__6;
lean_object* l___regBuiltinParser_Lean_Parser_Term_borrowed(lean_object*);
lean_object* l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__11;
lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__4;
@ -2079,6 +2109,7 @@ lean_object* l_Lean_Parser_Term_unicodeInfixL___elambda__1(lean_object*, lean_ob
lean_object* l_Lean_Parser_Term_nativeRefl___elambda__1___closed__9;
lean_object* l_Lean_Parser_Term_subtype___closed__11;
lean_object* l_Lean_Parser_unicodeSymbolFnAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_levelStxQuot___closed__2;
lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__7;
lean_object* l_Lean_Parser_Term_namedArgument___closed__4;
lean_object* l_Lean_Parser_Term_dollar___closed__2;
@ -2096,6 +2127,7 @@ lean_object* l_Lean_Parser_Term_bnot___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_matchAlts___elambda__1___spec__15___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_let;
lean_object* l_Lean_Parser_Term_depArrow___closed__3;
lean_object* l_Lean_Parser_Term_funBinderStxQuot___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_namedHole___closed__1;
lean_object* l_Lean_Parser_Term_map;
lean_object* l_Lean_Parser_Term_unicodeInfixR(lean_object*, lean_object*, lean_object*);
@ -50904,6 +50936,618 @@ x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
lean_object* _init_l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("`(level|");
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__1;
x_2 = l_String_trim(x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Char_HasRepr___closed__1;
x_2 = l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__2;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__3;
x_2 = l_Char_HasRepr___closed__1;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__4;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
lean_object* l_Lean_Parser_Term_levelStxQuot___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_38; lean_object* x_39; lean_object* x_40;
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
x_4 = lean_array_get_size(x_3);
lean_dec(x_3);
x_38 = lean_ctor_get(x_2, 1);
lean_inc(x_38);
lean_inc(x_1);
x_39 = l_Lean_Parser_tokenFn(x_1, x_2);
x_40 = lean_ctor_get(x_39, 3);
lean_inc(x_40);
if (lean_obj_tag(x_40) == 0)
{
lean_object* x_41; lean_object* x_42;
x_41 = lean_ctor_get(x_39, 0);
lean_inc(x_41);
x_42 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_41);
lean_dec(x_41);
if (lean_obj_tag(x_42) == 2)
{
lean_object* x_43; lean_object* x_44; uint8_t x_45;
x_43 = lean_ctor_get(x_42, 1);
lean_inc(x_43);
lean_dec(x_42);
x_44 = l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__2;
x_45 = lean_string_dec_eq(x_43, x_44);
lean_dec(x_43);
if (x_45 == 0)
{
lean_object* x_46; lean_object* x_47;
x_46 = l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__5;
x_47 = l_Lean_Parser_ParserState_mkErrorsAt(x_39, x_46, x_38);
x_5 = x_47;
goto block_37;
}
else
{
lean_dec(x_38);
x_5 = x_39;
goto block_37;
}
}
else
{
lean_object* x_48; lean_object* x_49;
lean_dec(x_42);
x_48 = l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__5;
x_49 = l_Lean_Parser_ParserState_mkErrorsAt(x_39, x_48, x_38);
x_5 = x_49;
goto block_37;
}
}
else
{
lean_object* x_50; lean_object* x_51;
lean_dec(x_40);
x_50 = l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__5;
x_51 = l_Lean_Parser_ParserState_mkErrorsAt(x_39, x_50, x_38);
x_5 = x_51;
goto block_37;
}
block_37:
{
lean_object* x_6;
x_6 = lean_ctor_get(x_5, 3);
lean_inc(x_6);
if (lean_obj_tag(x_6) == 0)
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_7 = l_Lean_Parser_regBuiltinLevelParserAttr___closed__4;
x_8 = lean_unsigned_to_nat(0u);
lean_inc(x_1);
x_9 = l_Lean_Parser_categoryParser___elambda__1(x_7, x_8, x_1, x_5);
x_10 = lean_ctor_get(x_9, 3);
lean_inc(x_10);
if (lean_obj_tag(x_10) == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_11 = lean_ctor_get(x_9, 1);
lean_inc(x_11);
x_12 = l_Lean_Parser_tokenFn(x_1, x_9);
x_13 = lean_ctor_get(x_12, 3);
lean_inc(x_13);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_14; lean_object* x_15;
x_14 = lean_ctor_get(x_12, 0);
lean_inc(x_14);
x_15 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_14);
lean_dec(x_14);
if (lean_obj_tag(x_15) == 2)
{
lean_object* x_16; lean_object* x_17; uint8_t x_18;
x_16 = lean_ctor_get(x_15, 1);
lean_inc(x_16);
lean_dec(x_15);
x_17 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__4;
x_18 = lean_string_dec_eq(x_16, x_17);
lean_dec(x_16);
if (x_18 == 0)
{
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_19 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__7;
x_20 = l_Lean_Parser_ParserState_mkErrorsAt(x_12, x_19, x_11);
x_21 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_22 = l_Lean_Parser_ParserState_mkNode(x_20, x_21, x_4);
return x_22;
}
else
{
lean_object* x_23; lean_object* x_24;
lean_dec(x_11);
x_23 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_24 = l_Lean_Parser_ParserState_mkNode(x_12, x_23, x_4);
return x_24;
}
}
else
{
lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28;
lean_dec(x_15);
x_25 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__7;
x_26 = l_Lean_Parser_ParserState_mkErrorsAt(x_12, x_25, x_11);
x_27 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_28 = l_Lean_Parser_ParserState_mkNode(x_26, x_27, x_4);
return x_28;
}
}
else
{
lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32;
lean_dec(x_13);
x_29 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__7;
x_30 = l_Lean_Parser_ParserState_mkErrorsAt(x_12, x_29, x_11);
x_31 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_32 = l_Lean_Parser_ParserState_mkNode(x_30, x_31, x_4);
return x_32;
}
}
else
{
lean_object* x_33; lean_object* x_34;
lean_dec(x_10);
lean_dec(x_1);
x_33 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_34 = l_Lean_Parser_ParserState_mkNode(x_9, x_33, x_4);
return x_34;
}
}
else
{
lean_object* x_35; lean_object* x_36;
lean_dec(x_6);
lean_dec(x_1);
x_35 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_36 = l_Lean_Parser_ParserState_mkNode(x_5, x_35, x_4);
return x_36;
}
}
}
}
lean_object* _init_l_Lean_Parser_Term_levelStxQuot___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__2;
x_2 = l_Lean_Parser_Level_paren___closed__1;
x_3 = l_Lean_Parser_symbolInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_levelStxQuot___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_levelStxQuot___closed__1;
x_2 = l_Lean_Parser_Level_paren___closed__4;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_levelStxQuot___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_2 = l_Lean_Parser_Term_levelStxQuot___closed__2;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_levelStxQuot___closed__4() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_levelStxQuot___elambda__1), 2, 0);
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Term_levelStxQuot___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_levelStxQuot___closed__3;
x_2 = l_Lean_Parser_Term_levelStxQuot___closed__4;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_levelStxQuot() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Term_levelStxQuot___closed__5;
return x_1;
}
}
lean_object* _init_l___regBuiltinParser_Lean_Parser_Term_levelStxQuot___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("levelStxQuot");
return x_1;
}
}
lean_object* _init_l___regBuiltinParser_Lean_Parser_Term_levelStxQuot___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_mkAppStx___closed__6;
x_2 = l___regBuiltinParser_Lean_Parser_Term_levelStxQuot___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l___regBuiltinParser_Lean_Parser_Term_levelStxQuot(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l_Lean_Parser_termParser___closed__2;
x_3 = l___regBuiltinParser_Lean_Parser_Term_levelStxQuot___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Term_levelStxQuot;
x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
lean_object* _init_l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("`(funBinder|");
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__1;
x_2 = l_String_trim(x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Char_HasRepr___closed__1;
x_2 = l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__2;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__3;
x_2 = l_Char_HasRepr___closed__1;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__4;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
lean_object* l_Lean_Parser_Term_funBinderStxQuot___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_36; lean_object* x_37; lean_object* x_38;
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
x_4 = lean_array_get_size(x_3);
lean_dec(x_3);
x_36 = lean_ctor_get(x_2, 1);
lean_inc(x_36);
lean_inc(x_1);
x_37 = l_Lean_Parser_tokenFn(x_1, x_2);
x_38 = lean_ctor_get(x_37, 3);
lean_inc(x_38);
if (lean_obj_tag(x_38) == 0)
{
lean_object* x_39; lean_object* x_40;
x_39 = lean_ctor_get(x_37, 0);
lean_inc(x_39);
x_40 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_39);
lean_dec(x_39);
if (lean_obj_tag(x_40) == 2)
{
lean_object* x_41; lean_object* x_42; uint8_t x_43;
x_41 = lean_ctor_get(x_40, 1);
lean_inc(x_41);
lean_dec(x_40);
x_42 = l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__2;
x_43 = lean_string_dec_eq(x_41, x_42);
lean_dec(x_41);
if (x_43 == 0)
{
lean_object* x_44; lean_object* x_45;
x_44 = l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__5;
x_45 = l_Lean_Parser_ParserState_mkErrorsAt(x_37, x_44, x_36);
x_5 = x_45;
goto block_35;
}
else
{
lean_dec(x_36);
x_5 = x_37;
goto block_35;
}
}
else
{
lean_object* x_46; lean_object* x_47;
lean_dec(x_40);
x_46 = l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__5;
x_47 = l_Lean_Parser_ParserState_mkErrorsAt(x_37, x_46, x_36);
x_5 = x_47;
goto block_35;
}
}
else
{
lean_object* x_48; lean_object* x_49;
lean_dec(x_38);
x_48 = l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__5;
x_49 = l_Lean_Parser_ParserState_mkErrorsAt(x_37, x_48, x_36);
x_5 = x_49;
goto block_35;
}
block_35:
{
lean_object* x_6;
x_6 = lean_ctor_get(x_5, 3);
lean_inc(x_6);
if (lean_obj_tag(x_6) == 0)
{
lean_object* x_7; lean_object* x_8;
lean_inc(x_1);
x_7 = l_Lean_Parser_Term_funBinder___elambda__1(x_1, x_5);
x_8 = lean_ctor_get(x_7, 3);
lean_inc(x_8);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_9 = lean_ctor_get(x_7, 1);
lean_inc(x_9);
x_10 = l_Lean_Parser_tokenFn(x_1, x_7);
x_11 = lean_ctor_get(x_10, 3);
lean_inc(x_11);
if (lean_obj_tag(x_11) == 0)
{
lean_object* x_12; lean_object* x_13;
x_12 = lean_ctor_get(x_10, 0);
lean_inc(x_12);
x_13 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_12);
lean_dec(x_12);
if (lean_obj_tag(x_13) == 2)
{
lean_object* x_14; lean_object* x_15; uint8_t x_16;
x_14 = lean_ctor_get(x_13, 1);
lean_inc(x_14);
lean_dec(x_13);
x_15 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__4;
x_16 = lean_string_dec_eq(x_14, x_15);
lean_dec(x_14);
if (x_16 == 0)
{
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
x_17 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__7;
x_18 = l_Lean_Parser_ParserState_mkErrorsAt(x_10, x_17, x_9);
x_19 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_20 = l_Lean_Parser_ParserState_mkNode(x_18, x_19, x_4);
return x_20;
}
else
{
lean_object* x_21; lean_object* x_22;
lean_dec(x_9);
x_21 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_22 = l_Lean_Parser_ParserState_mkNode(x_10, x_21, x_4);
return x_22;
}
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
lean_dec(x_13);
x_23 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__7;
x_24 = l_Lean_Parser_ParserState_mkErrorsAt(x_10, x_23, x_9);
x_25 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_26 = l_Lean_Parser_ParserState_mkNode(x_24, x_25, x_4);
return x_26;
}
}
else
{
lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30;
lean_dec(x_11);
x_27 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__7;
x_28 = l_Lean_Parser_ParserState_mkErrorsAt(x_10, x_27, x_9);
x_29 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_30 = l_Lean_Parser_ParserState_mkNode(x_28, x_29, x_4);
return x_30;
}
}
else
{
lean_object* x_31; lean_object* x_32;
lean_dec(x_8);
lean_dec(x_1);
x_31 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_32 = l_Lean_Parser_ParserState_mkNode(x_7, x_31, x_4);
return x_32;
}
}
else
{
lean_object* x_33; lean_object* x_34;
lean_dec(x_6);
lean_dec(x_1);
x_33 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_34 = l_Lean_Parser_ParserState_mkNode(x_5, x_33, x_4);
return x_34;
}
}
}
}
lean_object* _init_l_Lean_Parser_Term_funBinderStxQuot___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__2;
x_2 = l_Lean_Parser_Level_paren___closed__1;
x_3 = l_Lean_Parser_symbolInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_funBinderStxQuot___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_funBinder;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___closed__3;
x_4 = l_Lean_Parser_andthenInfo(x_2, x_3);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Term_funBinderStxQuot___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_funBinderStxQuot___closed__1;
x_2 = l_Lean_Parser_Term_funBinderStxQuot___closed__2;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_funBinderStxQuot___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_2 = l_Lean_Parser_Term_funBinderStxQuot___closed__3;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_funBinderStxQuot___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_funBinderStxQuot___elambda__1), 2, 0);
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Term_funBinderStxQuot___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_funBinderStxQuot___closed__4;
x_2 = l_Lean_Parser_Term_funBinderStxQuot___closed__5;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_funBinderStxQuot() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Term_funBinderStxQuot___closed__6;
return x_1;
}
}
lean_object* _init_l___regBuiltinParser_Lean_Parser_Term_funBinderStxQuot___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("funBinderStxQuot");
return x_1;
}
}
lean_object* _init_l___regBuiltinParser_Lean_Parser_Term_funBinderStxQuot___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_mkAppStx___closed__6;
x_2 = l___regBuiltinParser_Lean_Parser_Term_funBinderStxQuot___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l___regBuiltinParser_Lean_Parser_Term_funBinderStxQuot(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l_Lean_Parser_termParser___closed__2;
x_3 = l___regBuiltinParser_Lean_Parser_Term_funBinderStxQuot___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Term_funBinderStxQuot;
x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
lean_object* initialize_Init_Lean_Parser_Parser(lean_object*);
lean_object* initialize_Init_Lean_Parser_Level(lean_object*);
static bool _G_initialized = false;
@ -54535,6 +55179,66 @@ lean_mark_persistent(l___regBuiltinParser_Lean_Parser_Term_tacticStxQuot___close
res = l___regBuiltinParser_Lean_Parser_Term_tacticStxQuot(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__1 = _init_l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__1();
lean_mark_persistent(l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__1);
l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__2 = _init_l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__2();
lean_mark_persistent(l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__2);
l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__3 = _init_l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__3();
lean_mark_persistent(l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__3);
l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__4 = _init_l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__4();
lean_mark_persistent(l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__4);
l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__5 = _init_l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__5();
lean_mark_persistent(l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__5);
l_Lean_Parser_Term_levelStxQuot___closed__1 = _init_l_Lean_Parser_Term_levelStxQuot___closed__1();
lean_mark_persistent(l_Lean_Parser_Term_levelStxQuot___closed__1);
l_Lean_Parser_Term_levelStxQuot___closed__2 = _init_l_Lean_Parser_Term_levelStxQuot___closed__2();
lean_mark_persistent(l_Lean_Parser_Term_levelStxQuot___closed__2);
l_Lean_Parser_Term_levelStxQuot___closed__3 = _init_l_Lean_Parser_Term_levelStxQuot___closed__3();
lean_mark_persistent(l_Lean_Parser_Term_levelStxQuot___closed__3);
l_Lean_Parser_Term_levelStxQuot___closed__4 = _init_l_Lean_Parser_Term_levelStxQuot___closed__4();
lean_mark_persistent(l_Lean_Parser_Term_levelStxQuot___closed__4);
l_Lean_Parser_Term_levelStxQuot___closed__5 = _init_l_Lean_Parser_Term_levelStxQuot___closed__5();
lean_mark_persistent(l_Lean_Parser_Term_levelStxQuot___closed__5);
l_Lean_Parser_Term_levelStxQuot = _init_l_Lean_Parser_Term_levelStxQuot();
lean_mark_persistent(l_Lean_Parser_Term_levelStxQuot);
l___regBuiltinParser_Lean_Parser_Term_levelStxQuot___closed__1 = _init_l___regBuiltinParser_Lean_Parser_Term_levelStxQuot___closed__1();
lean_mark_persistent(l___regBuiltinParser_Lean_Parser_Term_levelStxQuot___closed__1);
l___regBuiltinParser_Lean_Parser_Term_levelStxQuot___closed__2 = _init_l___regBuiltinParser_Lean_Parser_Term_levelStxQuot___closed__2();
lean_mark_persistent(l___regBuiltinParser_Lean_Parser_Term_levelStxQuot___closed__2);
res = l___regBuiltinParser_Lean_Parser_Term_levelStxQuot(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__1 = _init_l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__1();
lean_mark_persistent(l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__1);
l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__2 = _init_l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__2();
lean_mark_persistent(l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__2);
l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__3 = _init_l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__3();
lean_mark_persistent(l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__3);
l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__4 = _init_l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__4();
lean_mark_persistent(l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__4);
l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__5 = _init_l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__5();
lean_mark_persistent(l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__5);
l_Lean_Parser_Term_funBinderStxQuot___closed__1 = _init_l_Lean_Parser_Term_funBinderStxQuot___closed__1();
lean_mark_persistent(l_Lean_Parser_Term_funBinderStxQuot___closed__1);
l_Lean_Parser_Term_funBinderStxQuot___closed__2 = _init_l_Lean_Parser_Term_funBinderStxQuot___closed__2();
lean_mark_persistent(l_Lean_Parser_Term_funBinderStxQuot___closed__2);
l_Lean_Parser_Term_funBinderStxQuot___closed__3 = _init_l_Lean_Parser_Term_funBinderStxQuot___closed__3();
lean_mark_persistent(l_Lean_Parser_Term_funBinderStxQuot___closed__3);
l_Lean_Parser_Term_funBinderStxQuot___closed__4 = _init_l_Lean_Parser_Term_funBinderStxQuot___closed__4();
lean_mark_persistent(l_Lean_Parser_Term_funBinderStxQuot___closed__4);
l_Lean_Parser_Term_funBinderStxQuot___closed__5 = _init_l_Lean_Parser_Term_funBinderStxQuot___closed__5();
lean_mark_persistent(l_Lean_Parser_Term_funBinderStxQuot___closed__5);
l_Lean_Parser_Term_funBinderStxQuot___closed__6 = _init_l_Lean_Parser_Term_funBinderStxQuot___closed__6();
lean_mark_persistent(l_Lean_Parser_Term_funBinderStxQuot___closed__6);
l_Lean_Parser_Term_funBinderStxQuot = _init_l_Lean_Parser_Term_funBinderStxQuot();
lean_mark_persistent(l_Lean_Parser_Term_funBinderStxQuot);
l___regBuiltinParser_Lean_Parser_Term_funBinderStxQuot___closed__1 = _init_l___regBuiltinParser_Lean_Parser_Term_funBinderStxQuot___closed__1();
lean_mark_persistent(l___regBuiltinParser_Lean_Parser_Term_funBinderStxQuot___closed__1);
l___regBuiltinParser_Lean_Parser_Term_funBinderStxQuot___closed__2 = _init_l___regBuiltinParser_Lean_Parser_Term_funBinderStxQuot___closed__2();
lean_mark_persistent(l___regBuiltinParser_Lean_Parser_Term_funBinderStxQuot___closed__2);
res = l___regBuiltinParser_Lean_Parser_Term_funBinderStxQuot(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_mk_io_result(lean_box(0));
}
#ifdef __cplusplus

755
stage0/stdlib/Init/Lean/Util/Recognizers.c Normal file
View file

@ -0,0 +1,755 @@
// Lean compiler output
// Module: Init.Lean.Util.Recognizers
// Imports: Init.Lean.Expr
#include "runtime/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
lean_object* l_List_reverse___rarg(lean_object*);
lean_object* l_Lean_Expr_eq_x3f___closed__1;
lean_object* l_Lean_Expr_prod_x3f___closed__2;
lean_object* l_Lean_Expr_iff_x3f(lean_object*);
lean_object* l_Lean_Expr_eq_x3f___closed__2;
lean_object* l_Lean_Expr_eq_x3f___boxed(lean_object*);
lean_object* l_Lean_Expr_appFn_x21(lean_object*);
lean_object* l_Lean_Expr_listLitAux___main___closed__5;
lean_object* l_Lean_Expr_app4_x3f(lean_object*, lean_object*);
lean_object* l_Lean_Expr_appArg_x21(lean_object*);
lean_object* l_Lean_Expr_listLit_x3f(lean_object*);
lean_object* l_Lean_Expr_heq_x3f___closed__2;
lean_object* l_Lean_Expr_iff_x3f___closed__2;
lean_object* l_Lean_Expr_heq_x3f(lean_object*);
lean_object* l_Lean_Expr_app4_x3f___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Expr_eq_x3f(lean_object*);
lean_object* l_Lean_Expr_iff_x3f___boxed(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Expr_app3_x3f___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Expr_iff_x3f___closed__1;
lean_object* l_Lean_Expr_app2_x3f(lean_object*, lean_object*);
lean_object* l_Lean_Expr_listLitAux(lean_object*, lean_object*);
lean_object* l_Lean_Expr_listLitAux___main___closed__4;
uint8_t l_Lean_Expr_isAppOfArity___main(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_listLitAux___main(lean_object*, lean_object*);
lean_object* l_Lean_Expr_app3_x3f(lean_object*, lean_object*);
lean_object* l_Lean_Expr_heq_x3f___closed__1;
lean_object* l_Lean_Expr_heq_x3f___boxed(lean_object*);
lean_object* l_Lean_Expr_app1_x3f___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Expr_app2_x3f___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Expr_listLitAux___main___closed__6;
lean_object* l_Lean_Expr_arrow_x3f(lean_object*);
lean_object* l_Lean_Expr_listLitAux___main___closed__2;
lean_object* l_Lean_Expr_app1_x3f(lean_object*, lean_object*);
lean_object* l_Lean_Expr_arrayLit_x3f___closed__1;
lean_object* l_Lean_Expr_arrayLit_x3f___boxed(lean_object*);
lean_object* l_Lean_Expr_arrayLit_x3f(lean_object*);
uint8_t l_Lean_Expr_hasLooseBVars(lean_object*);
lean_object* l_Lean_Expr_arrow_x3f___boxed(lean_object*);
lean_object* l_Lean_Expr_prod_x3f___closed__1;
lean_object* l_Lean_Expr_arrayLit_x3f___closed__2;
lean_object* l_Lean_Expr_prod_x3f(lean_object*);
lean_object* l_Lean_Expr_prod_x3f___boxed(lean_object*);
lean_object* l_Lean_Expr_listLitAux___main___closed__3;
lean_object* l_Lean_Expr_listLitAux___main___closed__1;
lean_object* l_Lean_Expr_app1_x3f(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; uint8_t x_4;
x_3 = lean_unsigned_to_nat(1u);
x_4 = l_Lean_Expr_isAppOfArity___main(x_1, x_2, x_3);
if (x_4 == 0)
{
lean_object* x_5;
x_5 = lean_box(0);
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7;
x_6 = l_Lean_Expr_appArg_x21(x_1);
x_7 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_7, 0, x_6);
return x_7;
}
}
}
lean_object* l_Lean_Expr_app1_x3f___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Expr_app1_x3f(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l_Lean_Expr_app2_x3f(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; uint8_t x_4;
x_3 = lean_unsigned_to_nat(2u);
x_4 = l_Lean_Expr_isAppOfArity___main(x_1, x_2, x_3);
if (x_4 == 0)
{
lean_object* x_5;
x_5 = lean_box(0);
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_6 = l_Lean_Expr_appFn_x21(x_1);
x_7 = l_Lean_Expr_appArg_x21(x_6);
lean_dec(x_6);
x_8 = l_Lean_Expr_appArg_x21(x_1);
x_9 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_9, 0, x_7);
lean_ctor_set(x_9, 1, x_8);
x_10 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_10, 0, x_9);
return x_10;
}
}
}
lean_object* l_Lean_Expr_app2_x3f___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Expr_app2_x3f(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l_Lean_Expr_app3_x3f(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; uint8_t x_4;
x_3 = lean_unsigned_to_nat(3u);
x_4 = l_Lean_Expr_isAppOfArity___main(x_1, x_2, x_3);
if (x_4 == 0)
{
lean_object* x_5;
x_5 = lean_box(0);
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_6 = l_Lean_Expr_appFn_x21(x_1);
x_7 = l_Lean_Expr_appFn_x21(x_6);
x_8 = l_Lean_Expr_appArg_x21(x_7);
lean_dec(x_7);
x_9 = l_Lean_Expr_appArg_x21(x_6);
lean_dec(x_6);
x_10 = l_Lean_Expr_appArg_x21(x_1);
x_11 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_11, 0, x_9);
lean_ctor_set(x_11, 1, x_10);
x_12 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_12, 0, x_8);
lean_ctor_set(x_12, 1, x_11);
x_13 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_13, 0, x_12);
return x_13;
}
}
}
lean_object* l_Lean_Expr_app3_x3f___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Expr_app3_x3f(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l_Lean_Expr_app4_x3f(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; uint8_t x_4;
x_3 = lean_unsigned_to_nat(4u);
x_4 = l_Lean_Expr_isAppOfArity___main(x_1, x_2, x_3);
if (x_4 == 0)
{
lean_object* x_5;
x_5 = lean_box(0);
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_6 = l_Lean_Expr_appFn_x21(x_1);
x_7 = l_Lean_Expr_appFn_x21(x_6);
x_8 = l_Lean_Expr_appFn_x21(x_7);
x_9 = l_Lean_Expr_appArg_x21(x_8);
lean_dec(x_8);
x_10 = l_Lean_Expr_appArg_x21(x_7);
lean_dec(x_7);
x_11 = l_Lean_Expr_appArg_x21(x_6);
lean_dec(x_6);
x_12 = l_Lean_Expr_appArg_x21(x_1);
x_13 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_13, 0, x_11);
lean_ctor_set(x_13, 1, x_12);
x_14 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_14, 0, x_10);
lean_ctor_set(x_14, 1, x_13);
x_15 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_15, 0, x_9);
lean_ctor_set(x_15, 1, x_14);
x_16 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_16, 0, x_15);
return x_16;
}
}
}
lean_object* l_Lean_Expr_app4_x3f___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Expr_app4_x3f(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* _init_l_Lean_Expr_eq_x3f___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Eq");
return x_1;
}
}
lean_object* _init_l_Lean_Expr_eq_x3f___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Expr_eq_x3f___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Expr_eq_x3f(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4;
x_2 = l_Lean_Expr_eq_x3f___closed__2;
x_3 = lean_unsigned_to_nat(3u);
x_4 = l_Lean_Expr_isAppOfArity___main(x_1, x_2, x_3);
if (x_4 == 0)
{
lean_object* x_5;
x_5 = lean_box(0);
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_6 = l_Lean_Expr_appFn_x21(x_1);
x_7 = l_Lean_Expr_appFn_x21(x_6);
x_8 = l_Lean_Expr_appArg_x21(x_7);
lean_dec(x_7);
x_9 = l_Lean_Expr_appArg_x21(x_6);
lean_dec(x_6);
x_10 = l_Lean_Expr_appArg_x21(x_1);
x_11 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_11, 0, x_9);
lean_ctor_set(x_11, 1, x_10);
x_12 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_12, 0, x_8);
lean_ctor_set(x_12, 1, x_11);
x_13 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_13, 0, x_12);
return x_13;
}
}
}
lean_object* l_Lean_Expr_eq_x3f___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Expr_eq_x3f(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Expr_iff_x3f___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Iff");
return x_1;
}
}
lean_object* _init_l_Lean_Expr_iff_x3f___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Expr_iff_x3f___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Expr_iff_x3f(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4;
x_2 = l_Lean_Expr_iff_x3f___closed__2;
x_3 = lean_unsigned_to_nat(2u);
x_4 = l_Lean_Expr_isAppOfArity___main(x_1, x_2, x_3);
if (x_4 == 0)
{
lean_object* x_5;
x_5 = lean_box(0);
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_6 = l_Lean_Expr_appFn_x21(x_1);
x_7 = l_Lean_Expr_appArg_x21(x_6);
lean_dec(x_6);
x_8 = l_Lean_Expr_appArg_x21(x_1);
x_9 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_9, 0, x_7);
lean_ctor_set(x_9, 1, x_8);
x_10 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_10, 0, x_9);
return x_10;
}
}
}
lean_object* l_Lean_Expr_iff_x3f___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Expr_iff_x3f(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Expr_heq_x3f___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("HEq");
return x_1;
}
}
lean_object* _init_l_Lean_Expr_heq_x3f___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Expr_heq_x3f___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Expr_heq_x3f(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4;
x_2 = l_Lean_Expr_heq_x3f___closed__2;
x_3 = lean_unsigned_to_nat(4u);
x_4 = l_Lean_Expr_isAppOfArity___main(x_1, x_2, x_3);
if (x_4 == 0)
{
lean_object* x_5;
x_5 = lean_box(0);
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_6 = l_Lean_Expr_appFn_x21(x_1);
x_7 = l_Lean_Expr_appFn_x21(x_6);
x_8 = l_Lean_Expr_appFn_x21(x_7);
x_9 = l_Lean_Expr_appArg_x21(x_8);
lean_dec(x_8);
x_10 = l_Lean_Expr_appArg_x21(x_7);
lean_dec(x_7);
x_11 = l_Lean_Expr_appArg_x21(x_6);
lean_dec(x_6);
x_12 = l_Lean_Expr_appArg_x21(x_1);
x_13 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_13, 0, x_11);
lean_ctor_set(x_13, 1, x_12);
x_14 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_14, 0, x_10);
lean_ctor_set(x_14, 1, x_13);
x_15 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_15, 0, x_9);
lean_ctor_set(x_15, 1, x_14);
x_16 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_16, 0, x_15);
return x_16;
}
}
}
lean_object* l_Lean_Expr_heq_x3f___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Expr_heq_x3f(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_Expr_arrow_x3f(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 7)
{
lean_object* x_2; lean_object* x_3; uint8_t x_4;
x_2 = lean_ctor_get(x_1, 1);
x_3 = lean_ctor_get(x_1, 2);
x_4 = l_Lean_Expr_hasLooseBVars(x_3);
if (x_4 == 0)
{
lean_object* x_5; lean_object* x_6;
lean_inc(x_3);
lean_inc(x_2);
x_5 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_5, 0, x_2);
lean_ctor_set(x_5, 1, x_3);
x_6 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_6, 0, x_5);
return x_6;
}
else
{
lean_object* x_7;
x_7 = lean_box(0);
return x_7;
}
}
else
{
lean_object* x_8;
x_8 = lean_box(0);
return x_8;
}
}
}
lean_object* l_Lean_Expr_arrow_x3f___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Expr_arrow_x3f(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Expr_listLitAux___main___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("List");
return x_1;
}
}
lean_object* _init_l_Lean_Expr_listLitAux___main___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Expr_listLitAux___main___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Expr_listLitAux___main___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("nil");
return x_1;
}
}
lean_object* _init_l_Lean_Expr_listLitAux___main___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Expr_listLitAux___main___closed__2;
x_2 = l_Lean_Expr_listLitAux___main___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Expr_listLitAux___main___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("cons");
return x_1;
}
}
lean_object* _init_l_Lean_Expr_listLitAux___main___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Expr_listLitAux___main___closed__2;
x_2 = l_Lean_Expr_listLitAux___main___closed__5;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Expr_listLitAux___main(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; uint8_t x_5;
x_3 = l_Lean_Expr_listLitAux___main___closed__4;
x_4 = lean_unsigned_to_nat(1u);
x_5 = l_Lean_Expr_isAppOfArity___main(x_1, x_3, x_4);
if (x_5 == 0)
{
lean_object* x_6; lean_object* x_7; uint8_t x_8;
x_6 = l_Lean_Expr_listLitAux___main___closed__6;
x_7 = lean_unsigned_to_nat(3u);
x_8 = l_Lean_Expr_isAppOfArity___main(x_1, x_6, x_7);
if (x_8 == 0)
{
lean_object* x_9;
lean_dec(x_2);
lean_dec(x_1);
x_9 = lean_box(0);
return x_9;
}
else
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_10 = l_Lean_Expr_appArg_x21(x_1);
x_11 = l_Lean_Expr_appFn_x21(x_1);
lean_dec(x_1);
x_12 = l_Lean_Expr_appArg_x21(x_11);
lean_dec(x_11);
x_13 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_13, 0, x_12);
lean_ctor_set(x_13, 1, x_2);
x_1 = x_10;
x_2 = x_13;
goto _start;
}
}
else
{
lean_object* x_15; lean_object* x_16;
lean_dec(x_1);
x_15 = l_List_reverse___rarg(x_2);
x_16 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_16, 0, x_15);
return x_16;
}
}
}
lean_object* l_Lean_Expr_listLitAux(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Expr_listLitAux___main(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Expr_listLit_x3f(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = lean_box(0);
x_3 = l_Lean_Expr_listLitAux___main(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Expr_arrayLit_x3f___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("toArray");
return x_1;
}
}
lean_object* _init_l_Lean_Expr_arrayLit_x3f___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Expr_listLitAux___main___closed__2;
x_2 = l_Lean_Expr_arrayLit_x3f___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Expr_arrayLit_x3f(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_8; lean_object* x_9; uint8_t x_10;
x_8 = l_Lean_Expr_arrayLit_x3f___closed__2;
x_9 = lean_unsigned_to_nat(2u);
x_10 = l_Lean_Expr_isAppOfArity___main(x_1, x_8, x_9);
if (x_10 == 0)
{
lean_object* x_11;
x_11 = lean_box(0);
x_2 = x_11;
goto block_7;
}
else
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_12 = l_Lean_Expr_appFn_x21(x_1);
x_13 = l_Lean_Expr_appArg_x21(x_12);
lean_dec(x_12);
x_14 = l_Lean_Expr_appArg_x21(x_1);
x_15 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_15, 0, x_13);
lean_ctor_set(x_15, 1, x_14);
x_16 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_16, 0, x_15);
x_2 = x_16;
goto block_7;
}
block_7:
{
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_3;
x_3 = lean_box(0);
return x_3;
}
else
{
lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_ctor_get(x_2, 0);
lean_inc(x_4);
lean_dec(x_2);
x_5 = lean_ctor_get(x_4, 1);
lean_inc(x_5);
lean_dec(x_4);
x_6 = l_Lean_Expr_listLit_x3f(x_5);
return x_6;
}
}
}
}
lean_object* l_Lean_Expr_arrayLit_x3f___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Expr_arrayLit_x3f(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Expr_prod_x3f___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Prod");
return x_1;
}
}
lean_object* _init_l_Lean_Expr_prod_x3f___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Expr_prod_x3f___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Expr_prod_x3f(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4;
x_2 = l_Lean_Expr_prod_x3f___closed__2;
x_3 = lean_unsigned_to_nat(2u);
x_4 = l_Lean_Expr_isAppOfArity___main(x_1, x_2, x_3);
if (x_4 == 0)
{
lean_object* x_5;
x_5 = lean_box(0);
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_6 = l_Lean_Expr_appFn_x21(x_1);
x_7 = l_Lean_Expr_appArg_x21(x_6);
lean_dec(x_6);
x_8 = l_Lean_Expr_appArg_x21(x_1);
x_9 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_9, 0, x_7);
lean_ctor_set(x_9, 1, x_8);
x_10 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_10, 0, x_9);
return x_10;
}
}
}
lean_object* l_Lean_Expr_prod_x3f___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Expr_prod_x3f(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* initialize_Init_Lean_Expr(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_Util_Recognizers(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;
res = initialize_Init_Lean_Expr(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Expr_eq_x3f___closed__1 = _init_l_Lean_Expr_eq_x3f___closed__1();
lean_mark_persistent(l_Lean_Expr_eq_x3f___closed__1);
l_Lean_Expr_eq_x3f___closed__2 = _init_l_Lean_Expr_eq_x3f___closed__2();
lean_mark_persistent(l_Lean_Expr_eq_x3f___closed__2);
l_Lean_Expr_iff_x3f___closed__1 = _init_l_Lean_Expr_iff_x3f___closed__1();
lean_mark_persistent(l_Lean_Expr_iff_x3f___closed__1);
l_Lean_Expr_iff_x3f___closed__2 = _init_l_Lean_Expr_iff_x3f___closed__2();
lean_mark_persistent(l_Lean_Expr_iff_x3f___closed__2);
l_Lean_Expr_heq_x3f___closed__1 = _init_l_Lean_Expr_heq_x3f___closed__1();
lean_mark_persistent(l_Lean_Expr_heq_x3f___closed__1);
l_Lean_Expr_heq_x3f___closed__2 = _init_l_Lean_Expr_heq_x3f___closed__2();
lean_mark_persistent(l_Lean_Expr_heq_x3f___closed__2);
l_Lean_Expr_listLitAux___main___closed__1 = _init_l_Lean_Expr_listLitAux___main___closed__1();
lean_mark_persistent(l_Lean_Expr_listLitAux___main___closed__1);
l_Lean_Expr_listLitAux___main___closed__2 = _init_l_Lean_Expr_listLitAux___main___closed__2();
lean_mark_persistent(l_Lean_Expr_listLitAux___main___closed__2);
l_Lean_Expr_listLitAux___main___closed__3 = _init_l_Lean_Expr_listLitAux___main___closed__3();
lean_mark_persistent(l_Lean_Expr_listLitAux___main___closed__3);
l_Lean_Expr_listLitAux___main___closed__4 = _init_l_Lean_Expr_listLitAux___main___closed__4();
lean_mark_persistent(l_Lean_Expr_listLitAux___main___closed__4);
l_Lean_Expr_listLitAux___main___closed__5 = _init_l_Lean_Expr_listLitAux___main___closed__5();
lean_mark_persistent(l_Lean_Expr_listLitAux___main___closed__5);
l_Lean_Expr_listLitAux___main___closed__6 = _init_l_Lean_Expr_listLitAux___main___closed__6();
lean_mark_persistent(l_Lean_Expr_listLitAux___main___closed__6);
l_Lean_Expr_arrayLit_x3f___closed__1 = _init_l_Lean_Expr_arrayLit_x3f___closed__1();
lean_mark_persistent(l_Lean_Expr_arrayLit_x3f___closed__1);
l_Lean_Expr_arrayLit_x3f___closed__2 = _init_l_Lean_Expr_arrayLit_x3f___closed__2();
lean_mark_persistent(l_Lean_Expr_arrayLit_x3f___closed__2);
l_Lean_Expr_prod_x3f___closed__1 = _init_l_Lean_Expr_prod_x3f___closed__1();
lean_mark_persistent(l_Lean_Expr_prod_x3f___closed__1);
l_Lean_Expr_prod_x3f___closed__2 = _init_l_Lean_Expr_prod_x3f___closed__2();
lean_mark_persistent(l_Lean_Expr_prod_x3f___closed__2);
return lean_mk_io_result(lean_box(0));
}
#ifdef __cplusplus
}
#endif

6
stage0/stdlib/Init/LeanInit.c
View file

@ -4627,7 +4627,6 @@ x_47 = lean_nat_add(x_46, x_40);
lean_dec(x_40);
lean_dec(x_46);
x_48 = l_Char_ofNat(x_47);
lean_dec(x_47);
x_49 = lean_box_uint32(x_48);
lean_ctor_set(x_38, 0, x_49);
return x_35;
@ -4657,7 +4656,6 @@ x_58 = lean_nat_add(x_57, x_50);
lean_dec(x_50);
lean_dec(x_57);
x_59 = l_Char_ofNat(x_58);
lean_dec(x_58);
x_60 = lean_box_uint32(x_59);
x_61 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_61, 0, x_60);
@ -4701,7 +4699,6 @@ x_72 = lean_nat_add(x_71, x_63);
lean_dec(x_63);
lean_dec(x_71);
x_73 = l_Char_ofNat(x_72);
lean_dec(x_72);
x_74 = lean_box_uint32(x_73);
if (lean_is_scalar(x_65)) {
x_75 = lean_alloc_ctor(0, 2, 0);
@ -4771,7 +4768,6 @@ x_90 = lean_nat_add(x_89, x_87);
lean_dec(x_87);
lean_dec(x_89);
x_91 = l_Char_ofNat(x_90);
lean_dec(x_90);
x_92 = lean_box_uint32(x_91);
lean_ctor_set(x_85, 0, x_92);
return x_82;
@ -4791,7 +4787,6 @@ x_97 = lean_nat_add(x_96, x_93);
lean_dec(x_93);
lean_dec(x_96);
x_98 = l_Char_ofNat(x_97);
lean_dec(x_97);
x_99 = lean_box_uint32(x_98);
x_100 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_100, 0, x_99);
@ -4825,7 +4820,6 @@ x_107 = lean_nat_add(x_106, x_102);
lean_dec(x_102);
lean_dec(x_106);
x_108 = l_Char_ofNat(x_107);
lean_dec(x_107);
x_109 = lean_box_uint32(x_108);
if (lean_is_scalar(x_104)) {
x_110 = lean_alloc_ctor(0, 2, 0);