Lean.Elab.DefView

Lean.Elab.DefKind.isDefOrAbbrevOrOpaque x = match x with | Lean.Elab.DefKind.def => true | Lean.Elab.DefKind.opaque => true | Lean.Elab.DefKind.abbrev => true | x => false

source

def Lean.Elab.DefKind.isExample :

Lean.Elab.DefKind → Bool

Equations

Lean.Elab.DefKind.isExample x = match x with | Lean.Elab.DefKind.example => true | x => false

source

structure Lean.Elab.DefView :

Type

kind : Lean.Elab.DefKind
ref : Lean.Syntax
modifiers : Lean.Elab.Modifiers
declId : Lean.Syntax
binders : Lean.Syntax
type? : Option Lean.Syntax
value : Lean.Syntax
deriving? : Option (Array Lean.Syntax)

source

instance Lean.Elab.instInhabitedDefView :

Inhabited Lean.Elab.DefView

Equations

Lean.Elab.instInhabitedDefView = { default := { kind := default, ref := default, modifiers := default, declId := default, binders := default, type? := default, value := default, deriving? := default } }

source

def Lean.Elab.Command.mkDefViewOfAbbrev (modifiers : Lean.Elab.Modifiers) (stx : Lean.Syntax) :

Lean.Elab.DefView

Equations

Lean.Elab.Command.mkDefViewOfAbbrev modifiers stx = let x := Lean.Elab.expandOptDeclSig (Lean.Syntax.getOp stx 2); match x with | (binders, type) => let modifiers := Lean.Elab.Modifiers.addAttribute modifiers { kind := Lean.AttributeKind.global, name := `inline, stx := Lean.Syntax.missing }; let modifiers := Lean.Elab.Modifiers.addAttribute modifiers { kind := Lean.AttributeKind.global, name := `reducible, stx := Lean.Syntax.missing }; { kind := Lean.Elab.DefKind.abbrev, ref := stx, modifiers := modifiers, declId := Lean.Syntax.getOp stx 1, binders := binders, type? := type, value := Lean.Syntax.getOp stx 3, deriving? := none }

source

def Lean.Elab.Command.mkDefViewOfDef (modifiers : Lean.Elab.Modifiers) (stx : Lean.Syntax) :

Lean.Elab.DefView

Equations

Lean.Elab.Command.mkDefViewOfDef modifiers stx = let x := Lean.Elab.expandOptDeclSig (Lean.Syntax.getOp stx 2); match x with | (binders, type) => let deriving? := if Lean.Syntax.isNone (Lean.Syntax.getOp stx 4) = true then none else some (Lean.Syntax.getSepArgs (Lean.Syntax.getOp (Lean.Syntax.getOp stx 4) 1)); { kind := Lean.Elab.DefKind.def, ref := stx, modifiers := modifiers, declId := Lean.Syntax.getOp stx 1, binders := binders, type? := type, value := Lean.Syntax.getOp stx 3, deriving? := deriving? }

source

def Lean.Elab.Command.mkDefViewOfTheorem (modifiers : Lean.Elab.Modifiers) (stx : Lean.Syntax) :

Lean.Elab.DefView

Equations

Lean.Elab.Command.mkDefViewOfTheorem modifiers stx = let x := Lean.Elab.expandDeclSig (Lean.Syntax.getOp stx 2); match x with | (binders, type) => { kind := Lean.Elab.DefKind.theorem, ref := stx, modifiers := modifiers, declId := Lean.Syntax.getOp stx 1, binders := binders, type? := some type, value := Lean.Syntax.getOp stx 3, deriving? := none }

source

def Lean.Elab.Command.mkFreshInstanceName :

Lean.Elab.Command.CommandElabM Lean.Name

Equations

Lean.Elab.Command.mkFreshInstanceName = do let s ← get let idx : Nat := s.nextInstIdx modify fun s => { env := s.env, messages := s.messages, scopes := s.scopes, nextMacroScope := s.nextMacroScope, maxRecDepth := s.maxRecDepth, nextInstIdx := s.nextInstIdx + 1, ngen := s.ngen, infoState := s.infoState, traceState := s.traceState } pure (Lean.Elab.mkFreshInstanceName s.env idx)

source

def Lean.Elab.Command.mkInstanceName (binders : Array Lean.Syntax) (type : Lean.Syntax) :

Lean.Elab.Command.CommandElabM Lean.Name

Equations

Lean.Elab.Command.mkInstanceName binders type = do let savedState ← get tryCatch (do let result ← Lean.Elab.Command.runTermElabM (some `inst) fun x => Lean.Elab.Term.withAutoBoundImplicit (Lean.Elab.Term.elabBinders binders fun x => Lean.Elab.Term.withoutErrToSorry do let a ← Lean.Elab.Term.elabType type let type ← liftM (Lean.Meta.instantiateMVars a) let ref ← liftM (IO.mkRef "") liftM (Lean.Meta.forEachExpr type fun e => if Lean.Expr.isForall e = true then ST.Ref.modify ref fun a => a ++ "ForAll" else if Lean.Expr.isProp e = true then ST.Ref.modify ref fun a => a ++ "Prop" else if Lean.Expr.isType e = true then ST.Ref.modify ref fun a => a ++ "Type" else if Lean.Expr.isSort e = true then ST.Ref.modify ref fun a => a ++ "Sort" else if Lean.Expr.isConst e = true then match Lean.Name.eraseMacroScopes (Lean.Expr.constName! e) with | Lean.Name.str x str x_1 => if Char.isLower (String.getOp str 0) = true then ST.Ref.modify ref fun a => a ++ String.capitalize str else ST.Ref.modify ref fun a => a ++ str | x => pure () else pure PUnit.unit) ST.Ref.get ref) set savedState Lean.Elab.liftMacroM (Lean.Elab.mkUnusedBaseName (Lean.Name.mkSimple ("inst" ++ result)))) fun ex => do set savedState Lean.Elab.Command.mkFreshInstanceName

source

def Lean.Elab.Command.mkDefViewOfInstance (modifiers : Lean.Elab.Modifiers) (stx : Lean.Syntax) :

Lean.Elab.Command.CommandElabM Lean.Elab.DefView

Equations

Lean.Elab.Command.mkDefViewOfInstance modifiers stx = do let attrKind ← Lean.Elab.liftMacroM (Lean.Elab.toAttributeKind (Lean.Syntax.getOp stx 0)) let prio ← Lean.Elab.liftMacroM (Lean.Elab.expandOptNamedPrio (Lean.Syntax.getOp stx 2)) let attrStx ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Attr.instance #[Lean.Syntax.atom info "instance", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.quote prio]]) let x : Lean.Syntax × Lean.Syntax := Lean.Elab.expandDeclSig (Lean.Syntax.getOp stx 4) match x with | (binders, type) => let modifiers := Lean.Elab.Modifiers.addAttribute modifiers { kind := attrKind, name := `instance, stx := attrStx }; let _do_jp := fun declId => pure { kind := Lean.Elab.DefKind.def, ref := stx, modifiers := modifiers, declId := declId, binders := binders, type? := some type, value := Lean.Syntax.getOp stx 5, deriving? := none }; match Lean.Syntax.getOptional? (Lean.Syntax.getOp stx 3) with | some declId => do let y ← pure declId _do_jp y | none => do let id ← Lean.Elab.Command.mkInstanceName (Lean.Syntax.getArgs binders) type let y ← pure (Lean.mkNode `Lean.Parser.Command.declId #[Lean.mkIdentFrom stx id, Lean.mkNullNode]) _do_jp y

source

def Lean.Elab.Command.mkDefViewOfConstant (modifiers : Lean.Elab.Modifiers) (stx : Lean.Syntax) :

Lean.Elab.Command.CommandElabM Lean.Elab.DefView

Equations

Lean.Elab.Command.mkDefViewOfConstant modifiers stx = let x := Lean.Elab.expandDeclSig (Lean.Syntax.getOp stx 2); match x with | (binders, type) => let _do_jp := fun val => pure { kind := Lean.Elab.DefKind.opaque, ref := stx, modifiers := modifiers, declId := Lean.Syntax.getOp stx 1, binders := binders, type? := some type, value := val, deriving? := none }; match Lean.Syntax.getOptional? (Lean.Syntax.getOp stx 3) with | some val => do let y ← pure val _do_jp y | none => do let val ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.defaultOrOfNonempty #[Lean.Syntax.atom info "default_or_ofNonempty%"]) let y ← pure (Lean.mkNode `Lean.Parser.Command.declValSimple #[Lean.mkAtomFrom stx ":=", val]) _do_jp y

source

def Lean.Elab.Command.mkDefViewOfExample (modifiers : Lean.Elab.Modifiers) (stx : Lean.Syntax) :

Lean.Elab.DefView

Equations

Lean.Elab.Command.mkDefViewOfExample modifiers stx = let x := Lean.Elab.expandDeclSig (Lean.Syntax.getOp stx 1); match x with | (binders, type) => let id := Lean.mkIdentFrom stx `_example; let declId := Lean.mkNode `Lean.Parser.Command.declId #[id, Lean.mkNullNode]; { kind := Lean.Elab.DefKind.example, ref := stx, modifiers := modifiers, declId := declId, binders := binders, type? := some type, value := Lean.Syntax.getOp stx 2, deriving? := none }

source

def Lean.Elab.Command.isDefLike (stx : Lean.Syntax) :

Bool

Equations

Lean.Elab.Command.isDefLike stx = let declKind := Lean.Syntax.getKind stx; declKind == `Lean.Parser.Command.abbrev || declKind == `Lean.Parser.Command.def || declKind == `Lean.Parser.Command.theorem || declKind == `Lean.Parser.Command.constant || declKind == `Lean.Parser.Command.instance || declKind == `Lean.Parser.Command.example

source

def Lean.Elab.Command.mkDefView (modifiers : Lean.Elab.Modifiers) (stx : Lean.Syntax) :

Lean.Elab.Command.CommandElabM Lean.Elab.DefView

Equations

Lean.Elab.Command.mkDefView modifiers stx = let declKind := Lean.Syntax.getKind stx; if (declKind == `Lean.Parser.Command.abbrev) = true then pure (Lean.Elab.Command.mkDefViewOfAbbrev modifiers stx) else if (declKind == `Lean.Parser.Command.def) = true then pure (Lean.Elab.Command.mkDefViewOfDef modifiers stx) else if (declKind == `Lean.Parser.Command.theorem) = true then pure (Lean.Elab.Command.mkDefViewOfTheorem modifiers stx) else if (declKind == `Lean.Parser.Command.constant) = true then Lean.Elab.Command.mkDefViewOfConstant modifiers stx else if (declKind == `Lean.Parser.Command.instance) = true then Lean.Elab.Command.mkDefViewOfInstance modifiers stx else if (declKind == `Lean.Parser.Command.example) = true then pure (Lean.Elab.Command.mkDefViewOfExample modifiers stx) else Lean.throwError (Lean.toMessageData "unexpected kind of definition")