Lean.Elab.Deriving.Repr

def Lean.Elab.Deriving.Repr.mkReprHeader (ctx : Lean.Elab.Deriving.Context) (indVal : Lean.InductiveVal) :

Lean.Elab.TermElabM Lean.Elab.Deriving.Header

Equations

Lean.Elab.Deriving.Repr.mkReprHeader ctx indVal = do let _ ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.ident info (String.toSubstring "prec") (Lean.addMacroScope mainModule `prec scp) []) let header ← Lean.Elab.Deriving.mkHeader ctx `Repr 1 indVal let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.explicitBinder #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "prec") (Lean.addMacroScope mainModule `prec scp) []], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ":", Lean.Syntax.ident info (String.toSubstring "Nat") (Lean.addMacroScope mainModule `Nat scp) [(`Nat, [])]], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ")"]) pure { binders := Array.push header.binders a, argNames := header.argNames, targetNames := header.targetNames, targetType := header.targetType }

def Lean.Elab.Deriving.Repr.mkBodyForStruct (ctx : Lean.Elab.Deriving.Context) (header : Lean.Elab.Deriving.Header) (indVal : Lean.InductiveVal) :

Lean.Elab.TermElabM Lean.Syntax

Equations

Lean.Elab.Deriving.Repr.mkBodyForStruct ctx header indVal = do let ctorVal ← Lean.getConstInfoCtor (List.head! indVal.ctors) let a ← Lean.getEnv let fieldNames ← pure (Lean.getStructureFields a indVal.toConstantVal.name) let numParams : Nat := indVal.numParams let target : Lean.Syntax := Lean.mkIdent (Array.getOp header.targetNames 0) Lean.Meta.forallTelescopeReducing ctorVal.toConstantVal.type fun xs x => do let fields ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.ident info (String.toSubstring "Format.nil") (Lean.addMacroScope mainModule `Format.nil scp) [(`Std.Format.nil, [])]) let first : Bool := true let _do_jp : Bool → Lean.Syntax → PUnit → Lean.Elab.TermElabM Lean.Syntax := fun first fields y => do let r ← let col := { start := 0, stop := Array.size fieldNames, step := 1 }; forIn col { fst := first, snd := fields } fun i r => let first := r.fst; let fields := r.snd; let fieldName := Array.getOp fieldNames i; let fieldNameLit := Lean.Syntax.mkStrLit (toString fieldName); let x := Array.getOp xs (numParams + i); let _do_jp := fun first fields y => do let a ← liftM (Lean.Meta.isType x) <||> liftM (Lean.Meta.isProof x) if a = true then do let r ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `«term_++_» #[Lean.Syntax.node Lean.SourceInfo.none `«term_++_» #[Lean.Syntax.node Lean.SourceInfo.none `«term_++_» #[fields, Lean.Syntax.atom info "++", fieldNameLit], Lean.Syntax.atom info "++", Lean.Syntax.node Lean.SourceInfo.none `strLit #[Lean.Syntax.atom info "\" := \""]], Lean.Syntax.atom info "++", Lean.Syntax.node Lean.SourceInfo.none `strLit #[Lean.Syntax.atom info "\"_\""]]) let fields : Lean.Syntax := r pure PUnit.unit pure (ForInStep.yield { fst := first, snd := fields }) else do let r ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `«term_++_» #[Lean.Syntax.node Lean.SourceInfo.none `«term_++_» #[Lean.Syntax.node Lean.SourceInfo.none `«term_++_» #[fields, Lean.Syntax.atom info "++", fieldNameLit], Lean.Syntax.atom info "++", Lean.Syntax.node Lean.SourceInfo.none `strLit #[Lean.Syntax.atom info "\" := \""]], Lean.Syntax.atom info "++", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "repr") (Lean.addMacroScope mainModule `repr scp) [(`repr, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.proj #[target, Lean.Syntax.atom info ".", Lean.mkIdent fieldName], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]]) let fields : Lean.Syntax := r pure PUnit.unit pure (ForInStep.yield { fst := first, snd := fields }); if first = true then let first := false; do let y ← pure PUnit.unit _do_jp first fields y else do let r ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `«term_++_» #[Lean.Syntax.node Lean.SourceInfo.none `«term_++_» #[fields, Lean.Syntax.atom info "++", Lean.Syntax.node Lean.SourceInfo.none `strLit #[Lean.Syntax.atom info "\",\""]], Lean.Syntax.atom info "++", Lean.Syntax.ident info (String.toSubstring "Format.line") (Lean.addMacroScope mainModule `Format.line scp) [(`Std.Format.line, [])]]) let fields : Lean.Syntax := r let y ← pure PUnit.unit _do_jp first fields y let x : MProd Bool Lean.Syntax := r match x with | { fst := first, snd := fields } => do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Format.bracket") (Lean.addMacroScope mainModule `Format.bracket scp) [(`Std.Format.bracket, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `strLit #[Lean.Syntax.atom info "\"{ \""], fields, Lean.Syntax.node Lean.SourceInfo.none `strLit #[Lean.Syntax.atom info "\" }\""]]]) if (Array.size xs != numParams + Array.size fieldNames) = true then do let y ← Lean.throwError (Lean.toMessageData "'deriving Repr' failed, unexpected number of fields in structure") _do_jp first fields y else do let y ← pure PUnit.unit _do_jp first fields y

source

def Lean.Elab.Deriving.Repr.mkBodyForInduct (ctx : Lean.Elab.Deriving.Context) (header : Lean.Elab.Deriving.Header) (indVal : Lean.InductiveVal) (auxFunName : Lean.Name) :

Lean.Elab.TermElabM Lean.Syntax

Equations

Lean.Elab.Deriving.Repr.mkBodyForInduct ctx header indVal auxFunName = (fun mkAlts => do let discrs ← Lean.Elab.Deriving.mkDiscrs header indVal let alts ← mkAlts let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.match #[Lean.Syntax.atom info "match", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (Lean.mkSepArray (Array.map (fun discrs => discrs) discrs) (Lean.mkAtom ","))), Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "with", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlts #[Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] alts)]])) (Lean.Elab.Deriving.Repr.mkBodyForInduct.mkAlts indVal auxFunName)

source

def Lean.Elab.Deriving.Repr.mkBodyForInduct.mkAlts (indVal : Lean.InductiveVal) (auxFunName : Lean.Name) :

Lean.Elab.TermElabM (Array Lean.Syntax)

Equations

Lean.Elab.Deriving.Repr.mkBodyForInduct.mkAlts indVal auxFunName = let alts := #[]; do let r ← let col := indVal.ctors; forIn col alts fun ctorName r => let alts := r; do let ctorInfo ← Lean.getConstInfoCtor ctorName let alt ← Lean.Meta.forallTelescopeReducing ctorInfo.toConstantVal.type fun xs type => let patterns := #[]; do let r ← let col := { start := 0, stop := indVal.numIndices, step := 1 }; forIn col patterns fun i r => let patterns := r; do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"]) let patterns : Array Lean.Syntax := Array.push patterns a pure PUnit.unit pure (ForInStep.yield patterns) let x : Array Lean.Syntax := r let patterns : Array Lean.Syntax := x let ctorArgs : Array Lean.Syntax := #[] let rhs : Lean.Syntax := Lean.Syntax.mkStrLit (toString ctorInfo.toConstantVal.name) let r ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Format.text") (Lean.addMacroScope mainModule `Format.text scp) [(`Std.Format.text, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[rhs]]) let rhs : Lean.Syntax := r let r ← let col := { start := 0, stop := indVal.numParams, step := 1 }; forIn col ctorArgs fun i r => let ctorArgs := r; do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"]) let ctorArgs : Array Lean.Syntax := Array.push ctorArgs a pure PUnit.unit pure (ForInStep.yield ctorArgs) let x : Array Lean.Syntax := r let ctorArgs : Array Lean.Syntax := x let r ← let col := { start := 0, stop := ctorInfo.numFields, step := 1 }; forIn col { fst := ctorArgs, snd := rhs } fun i r => let ctorArgs := r.fst; let rhs := r.snd; let x := Array.getOp xs (indVal.numParams + i); do let a ← liftM (Lean.mkFreshUserName `a) let a : Lean.Syntax := Lean.mkIdent a let ctorArgs : Array Lean.Syntax := Array.push ctorArgs a let a_1 ← liftM (Lean.Meta.inferType x) if Lean.Expr.isAppOf a_1 indVal.toConstantVal.name = true then do let r ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `«term_++_» #[Lean.Syntax.node Lean.SourceInfo.none `«term_++_» #[rhs, Lean.Syntax.atom info "++", Lean.Syntax.ident info (String.toSubstring "Format.line") (Lean.addMacroScope mainModule `Format.line scp) [(`Std.Format.line, [])]], Lean.Syntax.atom info "++", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.mkIdent auxFunName, Lean.Syntax.node Lean.SourceInfo.none `null #[a, Lean.Syntax.node Lean.SourceInfo.none `termMax_prec #[Lean.Syntax.atom info "max_prec"]]]]) let rhs : Lean.Syntax := r pure PUnit.unit pure (ForInStep.yield { fst := ctorArgs, snd := rhs }) else do let r ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `«term_++_» #[Lean.Syntax.node Lean.SourceInfo.none `«term_++_» #[rhs, Lean.Syntax.atom info "++", Lean.Syntax.ident info (String.toSubstring "Format.line") (Lean.addMacroScope mainModule `Format.line scp) [(`Std.Format.line, [])]], Lean.Syntax.atom info "++", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "reprArg") (Lean.addMacroScope mainModule `reprArg scp) [(`reprArg, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[a]]]) let rhs : Lean.Syntax := r pure PUnit.unit pure (ForInStep.yield { fst := ctorArgs, snd := rhs }) let x : MProd (Array Lean.Syntax) Lean.Syntax := r match x with | { fst := ctorArgs, snd := rhs } => do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.explicit #[Lean.Syntax.atom info "@", Lean.mkIdent ctorName], Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] ctorArgs)]) let patterns : Array Lean.Syntax := Array.push patterns a let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (Lean.mkSepArray (Array.map (fun patterns => patterns) patterns) (Lean.mkAtom ","))), Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Repr.addAppParen") (Lean.addMacroScope mainModule `Repr.addAppParen scp) [(`Repr.addAppParen, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Format.group") (Lean.addMacroScope mainModule `Format.group scp) [(`Std.Format.group, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Format.nest") (Lean.addMacroScope mainModule `Format.nest scp) [(`Std.Format.nest, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `termIfThenElse #[Lean.Syntax.atom info "if", Lean.Syntax.node Lean.SourceInfo.none `«term_>=_» #[Lean.Syntax.ident info (String.toSubstring "prec") (Lean.addMacroScope mainModule `prec scp) [], Lean.Syntax.atom info ">=", Lean.Syntax.node Lean.SourceInfo.none `termMax_prec #[Lean.Syntax.atom info "max_prec"]], Lean.Syntax.atom info "then", Lean.Syntax.node Lean.SourceInfo.none `numLit #[Lean.Syntax.atom info "1"], Lean.Syntax.atom info "else", Lean.Syntax.node Lean.SourceInfo.none `numLit #[Lean.Syntax.atom info "2"]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[rhs, Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"], Lean.Syntax.ident info (String.toSubstring "prec") (Lean.addMacroScope mainModule `prec scp) []]]]) let alts : Array Lean.Syntax := Array.push alts alt pure PUnit.unit pure (ForInStep.yield alts) let x : Array Lean.Syntax := r let alts : Array Lean.Syntax := x pure alts

source

def Lean.Elab.Deriving.Repr.mkBody (ctx : Lean.Elab.Deriving.Context) (header : Lean.Elab.Deriving.Header) (indVal : Lean.InductiveVal) (auxFunName : Lean.Name) :

Lean.Elab.TermElabM Lean.Syntax

Equations

Lean.Elab.Deriving.Repr.mkBody ctx header indVal auxFunName = do let a ← Lean.getEnv if Lean.isStructure a indVal.toConstantVal.name = true then Lean.Elab.Deriving.Repr.mkBodyForStruct ctx header indVal else Lean.Elab.Deriving.Repr.mkBodyForInduct ctx header indVal auxFunName

source

def Lean.Elab.Deriving.Repr.mkAuxFunction (ctx : Lean.Elab.Deriving.Context) (i : Nat) :

Lean.Elab.TermElabM Lean.Syntax

Equations

Lean.Elab.Deriving.Repr.mkAuxFunction ctx i = do let auxFunName ← pure (Array.getOp ctx.auxFunNames i) let indVal ← pure (Array.getOp ctx.typeInfos i) let header ← Lean.Elab.Deriving.Repr.mkReprHeader ctx indVal let body ← Lean.Elab.Deriving.Repr.mkBody ctx header indVal auxFunName let _do_jp : Lean.Syntax → PUnit → Lean.Elab.TermElabM Lean.Syntax := fun body y => let binders := header.binders; if ctx.usePartial = true then do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declaration #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declModifiers #[Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.private #[Lean.Syntax.atom info "private"]], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.partial #[Lean.Syntax.atom info "partial"]]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.def #[Lean.Syntax.atom info "def", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declId #[Lean.mkIdent auxFunName, Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.optDeclSig #[Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] binders), Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeSpec #[Lean.Syntax.atom info ":", Lean.Syntax.ident info (String.toSubstring "Format") (Lean.addMacroScope mainModule `Format scp) [(`Std.Format, [])]]]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declValSimple #[Lean.Syntax.atom info ":=", body, Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]) else do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declaration #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declModifiers #[Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.private #[Lean.Syntax.atom info "private"]], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.def #[Lean.Syntax.atom info "def", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declId #[Lean.mkIdent auxFunName, Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.optDeclSig #[Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] binders), Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeSpec #[Lean.Syntax.atom info ":", Lean.Syntax.ident info (String.toSubstring "Format") (Lean.addMacroScope mainModule `Format scp) [(`Std.Format, [])]]]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declValSimple #[Lean.Syntax.atom info ":=", body, Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]) if ctx.usePartial = true then do let letDecls ← Lean.Elab.Deriving.mkLocalInstanceLetDecls ctx `Repr header.argNames let r ← Lean.Elab.Deriving.mkLet letDecls body let body : Lean.Syntax := r let y ← pure PUnit.unit _do_jp body y else do let y ← pure PUnit.unit _do_jp body y

source

def Lean.Elab.Deriving.Repr.mkMutualBlock (ctx : Lean.Elab.Deriving.Context) :

Lean.Elab.TermElabM Lean.Syntax

Equations

Lean.Elab.Deriving.Repr.mkMutualBlock ctx = let auxDefs := #[]; do let r ← let col := { start := 0, stop := Array.size ctx.typeInfos, step := 1 }; forIn col auxDefs fun i r => let auxDefs := r; do let a ← Lean.Elab.Deriving.Repr.mkAuxFunction ctx i let auxDefs : Array Lean.Syntax := Array.push auxDefs a pure PUnit.unit pure (ForInStep.yield auxDefs) let x : Array Lean.Syntax := r let auxDefs : Array Lean.Syntax := x let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.mutual #[Lean.Syntax.atom info "mutual", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] auxDefs), Lean.Syntax.atom info "end", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[]])

source

def Lean.Elab.Deriving.Repr.mkReprInstanceHandler (declNames : Array Lean.Name) :

Lean.Elab.Command.CommandElabM Bool

Equations

Lean.Elab.Deriving.Repr.mkReprInstanceHandler declNames = do let a ← Array.allM Lean.isInductive declNames 0 (Array.size declNames) if (a && decide (Array.size declNames > 0)) = true then do let cmds ← Lean.Elab.Command.liftTermElabM none (Lean.Elab.Deriving.Repr.mkReprInstanceCmds declNames) Array.forM Lean.Elab.Command.elabCommand cmds 0 (Array.size cmds) pure true else pure false