chore: update stage0
This commit is contained in:
Leonardo de Moura
parent
a10328e745
commit
29a28254ff
8 changed files with 7978 additions and 3719 deletions
20
stage0/src/Lean/Elab/App.lean
generated
20
stage0/src/Lean/Elab/App.lean
generated
|
|
@ -348,6 +348,21 @@ private def addImplicitArg (k : M Expr) : M Expr := do
|
|||
addNewArg arg
|
||||
k
|
||||
|
||||
/- Return true if there is a named argument that depends on the next argument. -/
|
||||
private def anyNamedArgDependsOnCurrent : M Bool := do
|
||||
let s ← get
|
||||
if s.namedArgs.isEmpty then
|
||||
return false
|
||||
else
|
||||
forallTelescopeReducing s.fType fun xs _ => do
|
||||
let curr := xs[0]
|
||||
for i in [1:xs.size] do
|
||||
let xDecl ← getLocalDecl xs[i].fvarId!
|
||||
if s.namedArgs.any fun arg => arg.name == xDecl.userName then
|
||||
if (← getMCtx).localDeclDependsOn xDecl curr.fvarId! then
|
||||
return true
|
||||
return false
|
||||
|
||||
/-
|
||||
Process a `fType` of the form `(x : A) → B x`.
|
||||
This method assume `fType` is a function type -/
|
||||
|
|
@ -383,7 +398,10 @@ private def processExplictArg (k : M Expr) : M Expr := do
|
|||
throwError "invalid autoParam, argument must be a constant"
|
||||
| _, _, _ =>
|
||||
if !s.namedArgs.isEmpty then
|
||||
addEtaArg k
|
||||
if (← anyNamedArgDependsOnCurrent) then
|
||||
addImplicitArg k
|
||||
else
|
||||
addEtaArg k
|
||||
else if !s.explicit then
|
||||
if (← fTypeHasOptAutoParams) then
|
||||
addEtaArg k
|
||||
|
|
|
|||
21
stage0/src/Lean/Elab/BuiltinNotation.lean
generated
21
stage0/src/Lean/Elab/BuiltinNotation.lean
generated
|
|
@ -43,23 +43,20 @@ open Meta
|
|||
|
||||
@[builtinMacro Lean.Parser.Term.have] def expandHave : Macro := fun stx =>
|
||||
let stx := stx.setArg 4 (mkNullNode #[mkAtomFrom stx ";"]) -- HACK
|
||||
let mkId (x? : Option Syntax) : Syntax :=
|
||||
x?.getD <| mkIdentFrom stx `this
|
||||
match stx with
|
||||
| `(have $type from $val; $body) => let thisId := mkIdentFrom stx `this; `(let! $thisId : $type := $val; $body)
|
||||
| `(have $type by $tac:tacticSeq; $body) => `(have $type from by $tac:tacticSeq; $body)
|
||||
| `(have $type := $val; $body) => let thisId := mkIdentFrom stx `this; `(let! $thisId : $type := $val; $body)
|
||||
| `(have $x : $type from $val; $body) => `(let! $x:ident : $type := $val; $body)
|
||||
| `(have $x : $type by $tac:tacticSeq; $body) => `(have $x : $type from by $tac:tacticSeq; $body)
|
||||
| `(have $x : $type := $val; $body) => `(let! $x:ident : $type := $val; $body)
|
||||
| _ => Macro.throwUnsupported
|
||||
| `(have $[$x :]? $type from $val $[;]? $body) => let x := mkId x; `(let! $x : $type := $val; $body)
|
||||
| `(have $[$x :]? $type := $val $[;]? $body) => let x := mkId x; `(let! $x : $type := $val; $body)
|
||||
| `(have $[$x :]? $type by $tac:tacticSeq $[;]? $body) => `(have $[$x :]? $type from by $tac:tacticSeq; $body)
|
||||
| _ => Macro.throwUnsupported
|
||||
|
||||
@[builtinMacro Lean.Parser.Term.suffices] def expandSuffices : Macro := fun stx =>
|
||||
let stx := stx.setArg 4 (mkNullNode #[mkAtomFrom stx ";"]) -- HACK
|
||||
match stx with
|
||||
| `(suffices $type from $val; $body) => `(have $type from $body; $val)
|
||||
| `(suffices $type by $tac:tacticSeq; $body) => `(have $type from $body; by $tac:tacticSeq)
|
||||
| `(suffices $x : $type from $val; $body) => `(have $x:ident : $type from $body; $val)
|
||||
| `(suffices $x : $type by $tac:tacticSeq; $body) => `(have $x:ident : $type from $body; by $tac:tacticSeq)
|
||||
| _ => Macro.throwUnsupported
|
||||
| `(suffices $[$x :]? $type from $val $[;]? $body) => `(have $[$x :]? $type from $body; $val)
|
||||
| `(suffices $[$x :]? $type by $tac:tacticSeq $[;]? $body) => `(have $[$x :]? $type from $body; by $tac:tacticSeq)
|
||||
| _ => Macro.throwUnsupported
|
||||
|
||||
private def elabParserMacroAux (prec : Syntax) (e : Syntax) : TermElabM Syntax := do
|
||||
let (some declName) ← getDeclName?
|
||||
|
|
|
|||
48
stage0/src/Lean/Elab/Syntax.lean
generated
48
stage0/src/Lean/Elab/Syntax.lean
generated
|
|
@ -378,26 +378,23 @@ def elabNoKindMacroRulesAux (alts : Array Syntax) : CommandElabM Syntax := do
|
|||
|
||||
@[builtinCommandElab «macro_rules»] def elabMacroRules : CommandElab :=
|
||||
adaptExpander fun stx => match stx with
|
||||
| `(macro_rules $alts:matchAlt*) => elabNoKindMacroRulesAux alts
|
||||
| `(macro_rules | $alts:matchAlt*) => elabNoKindMacroRulesAux alts
|
||||
| `(macro_rules [$kind] $alts:matchAlt*) => do elabMacroRulesAux ((← getCurrNamespace) ++ kind.getId) alts
|
||||
| `(macro_rules [$kind] | $alts:matchAlt*) => do elabMacroRulesAux ((← getCurrNamespace) ++ kind.getId) alts
|
||||
| _ => throwUnsupportedSyntax
|
||||
| `(macro_rules $[|]? $alts:matchAlt*) => elabNoKindMacroRulesAux alts
|
||||
| `(macro_rules [$kind] $[|]? $alts:matchAlt*) => do elabMacroRulesAux ((← getCurrNamespace) ++ kind.getId) alts
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
-- TODO: cleanup after we have support for optional syntax at `match_syntax`
|
||||
@[builtinMacro Lean.Parser.Command.mixfix] def expandMixfix : Macro := fun stx =>
|
||||
withAttrKindGlobal stx fun stx =>
|
||||
match stx with
|
||||
| `(infix:$prec $op => $f) => `(infixl:$prec $op => $f)
|
||||
| `(infixr:$prec $op => $f) => `(notation:$prec lhs $op:strLit rhs:$prec => $f lhs rhs)
|
||||
| `(infixl:$prec $op => $f) => let prec1 : Syntax := quote (prec.toNat+1); `(notation:$prec lhs $op:strLit rhs:$prec1 => $f lhs rhs)
|
||||
| `(prefix:$prec $op => $f) => `(notation:$prec $op:strLit arg:$prec => $f arg)
|
||||
| `(postfix:$prec $op => $f) => `(notation:$prec arg $op:strLit => $f arg)
|
||||
| `(infix:$prec [$prio] $op => $f) => `(infixl:$prec [$prio] $op => $f)
|
||||
| `(infixr:$prec [$prio] $op => $f) => `(notation:$prec [$prio] lhs $op:strLit rhs:$prec => $f lhs rhs)
|
||||
| `(infixl:$prec [$prio] $op => $f) => let prec1 : Syntax := quote (prec.toNat+1); `(notation:$prec [$prio] lhs $op:strLit rhs:$prec1 => $f lhs rhs)
|
||||
| `(prefix:$prec [$prio] $op => $f) => `(notation:$prec [$prio] $op:strLit arg:$prec => $f arg)
|
||||
| `(postfix:$prec [$prio] $op => $f) => `(notation:$prec [$prio] arg $op:strLit => $f arg)
|
||||
| `(infix $[: $prec]? $[[$prio]]? $op => $f) => `(infixl $[: $prec]? $[[$prio]]? $op => $f)
|
||||
| `(infixr $[: $prec]? $[[$prio]]? $op => $f) => `(notation $[: $prec]? $[[$prio]]? lhs $op:strLit rhs $[: $prec]? => $f lhs rhs)
|
||||
| `(infixl $[: $prec]? $[[$prio]]? $op => $f) =>
|
||||
let prec1 : Syntax := match (prec : Option Syntax) with
|
||||
| some prec => quote (prec.toNat+1)
|
||||
| none => quote 0
|
||||
`(notation $[: $prec]? $[[$prio]]? lhs $op:strLit rhs:$prec1 => $f lhs rhs)
|
||||
| `(prefix $[: $prec]? $[[$prio]]? $op => $f) => `(notation $[: $prec]? $[[$prio]]? $op:strLit arg $[: $prec]? => $f arg)
|
||||
| `(postfix $[: $prec]? $[[$prio]]? $op => $f) => `(notation $[: $prec]? $[[$prio]]? arg $op:strLit => $f arg)
|
||||
| _ => Macro.throwUnsupported
|
||||
where
|
||||
-- set "global" `attrKind`, apply `f`, and restore `attrKind` to result
|
||||
|
|
@ -463,7 +460,10 @@ def mkSimpleDelab (vars : Array Syntax) (pat qrhs : Syntax) : OptionT CommandEla
|
|||
| _ => throw ())
|
||||
|
||||
private def expandNotationAux (ref : Syntax)
|
||||
(currNamespace : Name) (attrKind : AttributeKind) (prec? : Option Syntax) (prio : Nat) (items : Array Syntax) (rhs : Syntax) : CommandElabM Syntax := do
|
||||
(currNamespace : Name) (attrKind : AttributeKind) (prec? : Option Syntax) (prio? : Option Syntax) (items : Array Syntax) (rhs : Syntax) : CommandElabM Syntax := do
|
||||
let prio := match prio? with
|
||||
| some prio => prio.isNatLit?.getD 0
|
||||
| _ => 0
|
||||
-- build parser
|
||||
let syntaxParts ← items.mapM expandNotationItemIntoSyntaxItem
|
||||
let cat := mkIdentFrom ref `term
|
||||
|
|
@ -477,13 +477,10 @@ private def expandNotationAux (ref : Syntax)
|
|||
So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/
|
||||
let fullKind := currNamespace ++ kind
|
||||
let pat := Syntax.node fullKind patArgs
|
||||
let stxDecl ← match prec?, attrKind with
|
||||
| none, AttributeKind.global => `(syntax [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat)
|
||||
| some prec, AttributeKind.global => `(syntax:$prec [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat)
|
||||
| none, AttributeKind.scoped => `(scoped syntax [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat)
|
||||
| some prec, AttributeKind.scoped => `(scoped syntax:$prec [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat)
|
||||
| none, AttributeKind.local => `(local syntax [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat)
|
||||
| some prec, AttributeKind.local => `(local syntax:$prec [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat)
|
||||
let stxDecl ← match attrKind with
|
||||
| AttributeKind.global => `(syntax $[: $prec?]? [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat)
|
||||
| AttributeKind.scoped => `(scoped syntax $[: $prec? ]? [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat)
|
||||
| AttributeKind.local => `(local syntax $[: $prec? ]? [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat)
|
||||
let macroDecl ← `(macro_rules | `($pat) => `($qrhs))
|
||||
match (← mkSimpleDelab vars pat qrhs |>.run) with
|
||||
| some delabDecl => mkNullNode #[stxDecl, macroDecl, delabDecl]
|
||||
|
|
@ -495,10 +492,7 @@ private def expandNotationAux (ref : Syntax)
|
|||
let stx := stx.setArg 0 mkAttrKindGlobal
|
||||
let currNamespace ← getCurrNamespace
|
||||
match stx with
|
||||
| `(notation:$prec $items* => $rhs) => expandNotationAux stx currNamespace attrKind prec 0 items rhs
|
||||
| `(notation $items:notationItem* => $rhs) => expandNotationAux stx currNamespace attrKind none 0 items rhs
|
||||
| `(notation:$prec [$prio] $items* => $rhs) => expandNotationAux stx currNamespace attrKind prec (prio.isNatLit?.getD 0) items rhs
|
||||
| `(notation [$prio] $items:notationItem* => $rhs) => expandNotationAux stx currNamespace attrKind none (prio.isNatLit?.getD 0) items rhs
|
||||
| `(notation $[: $prec? ]? $[[ $prio? ]]? $items* => $rhs) => expandNotationAux stx currNamespace attrKind prec? prio? items rhs
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
/- Convert `macro` argument into a `syntax` command item -/
|
||||
|
|
|
|||
9
stage0/src/Lean/Meta/Basic.lean
generated
9
stage0/src/Lean/Meta/Basic.lean
generated
|
|
@ -623,15 +623,15 @@ mutual
|
|||
k #[] type
|
||||
|
||||
private partial def isClassExpensive? : Expr → MetaM (Option Name)
|
||||
| type => withReducible $ -- when testing whether a type is a type class, we only unfold reducible constants.
|
||||
| type => withReducible <| -- when testing whether a type is a type class, we only unfold reducible constants.
|
||||
forallTelescopeReducingAux type none fun xs type => do
|
||||
match type.getAppFn with
|
||||
| Expr.const c _ _ => do
|
||||
let env ← getEnv
|
||||
pure $ if isClass env c then some c else none
|
||||
return if isClass env c then some c else none
|
||||
| _ => pure none
|
||||
|
||||
partial def isClass? (type : Expr) : MetaM (Option Name) := do
|
||||
private partial def isClassImp? (type : Expr) : MetaM (Option Name) := do
|
||||
match (← isClassQuick? type) with
|
||||
| LOption.none => pure none
|
||||
| LOption.some c => pure (some c)
|
||||
|
|
@ -639,6 +639,9 @@ mutual
|
|||
|
||||
end
|
||||
|
||||
def isClass? (type : Expr) : MetaM (Option Name) :=
|
||||
try isClassImp? type catch _ => pure none
|
||||
|
||||
private def withNewLocalInstancesImpAux {α} (fvars : Array Expr) (j : Nat) : n α → n α :=
|
||||
mapMetaM $ withNewLocalInstancesImp fvars j
|
||||
|
||||
|
|
|
|||
1550
stage0/stdlib/Lean/Elab/App.c
generated
1550
stage0/stdlib/Lean/Elab/App.c
generated
File diff suppressed because it is too large
Load diff
2616
stage0/stdlib/Lean/Elab/BuiltinNotation.c
generated
2616
stage0/stdlib/Lean/Elab/BuiltinNotation.c
generated
File diff suppressed because it is too large
Load diff
7382
stage0/stdlib/Lean/Elab/Syntax.c
generated
7382
stage0/stdlib/Lean/Elab/Syntax.c
generated
File diff suppressed because it is too large
Load diff
51
stage0/stdlib/Lean/Meta/Basic.c
generated
51
stage0/stdlib/Lean/Meta/Basic.c
generated
|
|
@ -316,7 +316,6 @@ lean_object* lean_level_update_max(lean_object*, lean_object*, lean_object*);
|
|||
lean_object* l_Lean_Meta_getPostponed___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_instMetaEvalMetaM___rarg___closed__2;
|
||||
lean_object* l_Lean_Meta_isDefEqStuckExceptionId;
|
||||
lean_object* l_Lean_Meta_isClass_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_mkArrow___closed__2;
|
||||
uint8_t l_Lean_Expr_hasExprMVar(lean_object*);
|
||||
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withNewFVar_match__1___rarg(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -483,6 +482,7 @@ lean_object* l_Lean_Meta_isDelayedAssigned___boxed(lean_object*, lean_object*, l
|
|||
lean_object* l_Lean_Meta_approxDefEq(lean_object*);
|
||||
lean_object* l_Lean_Meta_withExistingLocalDecls___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_getConstTemp_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_isClassImp_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_shouldReduceReducibleOnly___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_withExistingLocalDecls(lean_object*);
|
||||
uint8_t l_Lean_Meta_Config_foApprox___default;
|
||||
|
|
@ -540,7 +540,6 @@ lean_object* l_Lean_Meta_withAtLeastTransparency___rarg___lambda__1(uint8_t, lea
|
|||
lean_object* l_Lean_getReducibilityStatus___at___private_Lean_Meta_Basic_0__Lean_Meta_getDefInfoTemp___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_withAtLeastTransparency___rarg(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
|
||||
lean_object* l_Lean_Meta_saveAndResetSynthInstanceCache___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_isClass_x3f_match__1(lean_object*);
|
||||
lean_object* l_Lean_Meta_throwUnknownFVar___rarg___closed__2;
|
||||
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_instantiateForallAux_match__1(lean_object*);
|
||||
lean_object* l_Lean_MetavarContext_addExprMVarDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
|
||||
|
|
@ -766,10 +765,12 @@ lean_object* l_Lean_Meta_mapError___rarg___lambda__1(lean_object*, lean_object*,
|
|||
lean_object* l_Lean_Meta_forallTelescopeReducing___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_mkFreshLevelMVar___boxed(lean_object*);
|
||||
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_getDefInfoTemp_match__1(lean_object*);
|
||||
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_isClassImp_x3f_match__1(lean_object*);
|
||||
lean_object* l_Lean_Meta_forallBoundedTelescope___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_instInhabitedMetaM___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_lambdaTelescopeImp(lean_object*);
|
||||
lean_object* l_Lean_mkFreshId___at_Lean_Meta_mkFreshExprMVarAt___spec__1___rarg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_isClassImp_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_getFVarLocalDecl___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_lambdaTelescopeImp_process___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_instantiateLambdaAux_match__1(lean_object*);
|
||||
|
|
@ -17605,7 +17606,7 @@ x_2 = lean_alloc_closure((void*)(l___private_Lean_Meta_Basic_0__Lean_Meta_isClas
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Meta_isClass_x3f_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_isClassImp_x3f_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
switch (lean_obj_tag(x_1)) {
|
||||
|
|
@ -17641,11 +17642,11 @@ return x_10;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Meta_isClass_x3f_match__1(lean_object* x_1) {
|
||||
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_isClassImp_x3f_match__1(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_closure((void*)(l_Lean_Meta_isClass_x3f_match__1___rarg), 4, 0);
|
||||
x_2 = lean_alloc_closure((void*)(l___private_Lean_Meta_Basic_0__Lean_Meta_isClassImp_x3f_match__1___rarg), 4, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
|
|
@ -18728,7 +18729,7 @@ x_11 = l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAuxAux___
|
|||
return x_11;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Meta_isClass_x3f(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
|
||||
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_isClassImp_x3f(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_7;
|
||||
|
|
@ -18850,6 +18851,44 @@ return x_28;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Meta_isClass_x3f(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_7;
|
||||
x_7 = l___private_Lean_Meta_Basic_0__Lean_Meta_isClassImp_x3f(x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
if (lean_obj_tag(x_7) == 0)
|
||||
{
|
||||
return x_7;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_8;
|
||||
x_8 = !lean_is_exclusive(x_7);
|
||||
if (x_8 == 0)
|
||||
{
|
||||
lean_object* x_9; lean_object* x_10;
|
||||
x_9 = lean_ctor_get(x_7, 0);
|
||||
lean_dec(x_9);
|
||||
x_10 = lean_box(0);
|
||||
lean_ctor_set_tag(x_7, 0);
|
||||
lean_ctor_set(x_7, 0, x_10);
|
||||
return x_7;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_11; lean_object* x_12; lean_object* x_13;
|
||||
x_11 = lean_ctor_get(x_7, 1);
|
||||
lean_inc(x_11);
|
||||
lean_dec(x_7);
|
||||
x_12 = lean_box(0);
|
||||
x_13 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_13, 0, x_12);
|
||||
lean_ctor_set(x_13, 1, x_11);
|
||||
return x_13;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withNewLocalInstancesImpAux___rarg___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, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
|
||||
_start:
|
||||
{
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue