Lean.Elab.Declaration

Lean.Elab.Command.getTerminationHints stx = let decl := Lean.Syntax.getOp stx 1; let k := Lean.Syntax.getKind decl; if (k == `Lean.Parser.Command.def || k == `Lean.Parser.Command.theorem || k == `Lean.Parser.Command.instance) = true then let args := Lean.Syntax.getArgs decl; { terminationBy? := Lean.Syntax.getOptional? (Array.getOp args (Array.size args - 2)), decreasingBy? := Lean.Syntax.getOptional? (Array.getOp args (Array.size args - 1)) } else { terminationBy? := none, decreasingBy? := none }

source

def Lean.Elab.Command.expandMutualNamespace :

Lean.Macro

Equations

Lean.Elab.Command.expandMutualNamespace stx = let ns? := none; let elemsNew := #[]; do let r ← let col := Lean.Syntax.getArgs (Lean.Syntax.getOp stx 1); forIn col { fst := elemsNew, snd := ns? } fun elem r => let elemsNew := r.fst; let ns? := r.snd; do let a ← Lean.Elab.Command.expandDeclNamespace? elem match ns?, a with | x, none => let elemsNew := Array.push elemsNew elem; do pure PUnit.unit pure (ForInStep.yield { fst := elemsNew, snd := ns? }) | none, some (ns, elem) => let ns? := some ns; let elemsNew := Array.push elemsNew elem; do pure PUnit.unit pure (ForInStep.yield { fst := elemsNew, snd := ns? }) | some nsCurr, some (nsNew, elem) => if (nsCurr == nsNew) = true then let elemsNew := Array.push elemsNew elem; do pure PUnit.unit pure (ForInStep.yield { fst := elemsNew, snd := ns? }) else do Lean.Macro.throwErrorAt elem (toString "conflicting namespaces in mutual declaration, using namespace '" ++ toString nsNew ++ toString "', but used '" ++ toString nsCurr ++ toString "' in previous declaration") pure (ForInStep.yield { fst := elemsNew, snd := ns? }) let x : MProd (Array Lean.Syntax) (Option Lean.Name) := r match x with | { fst := elemsNew, snd := ns? } => match ns? with | some ns => let ns := Lean.mkIdentFrom stx ns; let stxNew := Lean.Syntax.setArg stx 1 (Lean.mkNullNode elemsNew); do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.namespace #[Lean.Syntax.atom info "namespace", ns], stxNew, Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.end #[Lean.Syntax.atom info "end", Lean.Syntax.node Lean.SourceInfo.none `null #[ns]]]) | none => Lean.Macro.throwUnsupported

source

def Lean.Elab.Command.expandMutualElement :

Lean.Macro

Equations

Lean.Elab.Command.expandMutualElement stx = let elemsNew := #[]; let modified := false; do let r ← let col := Lean.Syntax.getArgs (Lean.Syntax.getOp stx 1); forIn col { fst := elemsNew, snd := modified } fun elem r => let elemsNew := r.fst; let modified := r.snd; do let a ← Lean.expandMacro? elem match a with | some elemNew => let elemsNew := Array.push elemsNew elemNew; let modified := true; do pure PUnit.unit pure (ForInStep.yield { fst := elemsNew, snd := modified }) | none => let elemsNew := Array.push elemsNew elem; do pure PUnit.unit pure (ForInStep.yield { fst := elemsNew, snd := modified }) let x : MProd (Array Lean.Syntax) Bool := r match x with | { fst := elemsNew, snd := modified } => if modified = true then pure (Lean.Syntax.setArg stx 1 (Lean.mkNullNode elemsNew)) else Lean.Macro.throwUnsupported