Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2021 Gabriel Ebner. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gabriel Ebner
-/
import Lean
import Mathlib.Tactic.Eqns
import Mathlib.Data.Subtype

/-!
# Irreducible definitions

This file defines an `irreducible_def` command,
which works almost like the `def` command
except that the introduced definition
does not reduce to the value.
Instead, the command
adds a `_def` lemma
which can be used for rewriting.

```
irreducible_def frobnicate (a b : Nat) :=
  a + b

example : frobnicate a 0 = a := by
  simp [frobnicate_def]
```

-/

namespace Lean.Elab.Command

open Term Meta

/-- `delta% t` elaborates to a head-delta reduced version of `t`. -/
elab "delta% " 
t: ?m.103
t
:term : term <=
expectedType: ?m.70
expectedType
=> do let
t: ?m.355
t
←
elabTerm: Syntax → Option Expr → optParam Bool true → optParam Bool true → TermElabM Expr
elabTerm
t: ?m.103
t
expectedType: ?m.70
expectedType
synthesizeSyntheticMVars: optParam Bool true → optParam Bool false → TermElabM Unit
synthesizeSyntheticMVars
let
t: ?m.520
t
←
instantiateMVars: {m : Type → Type} → [inst : Monad m] → [inst : MonadMCtx m] → Expr → m Expr
instantiateMVars
t: ?m.355
t
let
some: {α : Type ?u.133} → α → Option α
some
t: Expr
t
←
delta?: Expr → (optParam (Name → Bool) fun x => true) → CoreM (Option Expr)
delta?
t: ?m.520
t
| throwError "cannot delta reduce {
t: ?m.520
t
}"
pure: {f : Type ?u.736 → Type ?u.735} → [self : Pure f] → {α : Type ?u.736} → α → f α
pure
t: Expr
t
/- `eta_helper f = (· + 3)` elabs to `∀ x, f x = x + 3` -/ local elab "eta_helper "
t: ?m.2856
t
:term : term => do let
t: ?m.3060
t
←
elabTerm: Syntax → Option Expr → optParam Bool true → optParam Bool true → TermElabM Expr
elabTerm
t: ?m.2856
t
none: {α : Type ?u.3049} → Option α
none
let
some: {α : Type ?u.3066} → α → Option α
some
(_,
lhs: Expr
lhs
,
rhs: Expr
rhs
) :=
t: ?m.3060
t
.
eq?: Expr → Option (Expr × Expr × Expr)
eq?
| throwError "not an equation: {
t: ?m.3060
t
}"
synthesizeSyntheticMVars: optParam Bool true → optParam Bool false → TermElabM Unit
synthesizeSyntheticMVars
let
rhs: ?m.3278
rhs
←
instantiateMVars: {m : Type → Type} → [inst : Monad m] → [inst : MonadMCtx m] → Expr → m Expr
instantiateMVars
rhs: Expr
rhs
lambdaTelescope: {n : Type → Type ?u.3280} → [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → Expr → (Array Expr → Expr → n α) → n α
lambdaTelescope
rhs: ?m.3278
rhs
fun
xs: ?m.3321
xs
rhs: ?m.3324
rhs
↦ do let
lhs: ?m.3332
lhs
:= (
mkAppN: Expr → Array Expr → Expr
mkAppN
lhs: Expr
lhs
xs: ?m.3321
xs
).
headBeta: Expr → Expr
headBeta
mkForallFVars: Array Expr → Expr → optParam Bool false → optParam Bool true → optParam BinderInfo BinderInfo.implicit → MetaM Expr
mkForallFVars
xs: ?m.3321
xs
<|←
mkEq: Expr → Expr → MetaM Expr
mkEq
lhs: ?m.3332
lhs
rhs: ?m.3324
rhs
/-- `val_proj x` elabs to the *primitive projection* `@x.val`. -/ local elab "val_proj "
e: ?m.6054
e
:term : term => do let
e: ?m.7102
e
←
elabTerm: Syntax → Option Expr → optParam Bool true → optParam Bool true → TermElabM Expr
elabTerm
(← `(($e : Subtype _))): ?m.6961
(← `(($
e: ?m.6054
e
(← `(($e : Subtype _))): ?m.6961
: Subtype _)))
none: {α : Type ?u.7091} → Option α
none
return
mkProj: Name → ℕ → Expr → Expr
mkProj
``
Subtype: {α : Sort u} → (α → Prop) → Sort (max1u)
Subtype
0: ?m.7130
0
e: ?m.7102
e
/-- Executes the commands, and stops after the first error. In short, S-A-F-E. -/ local syntax "stop_at_first_error" (ppLine command)* : command open Command in elab_rules : command | `(stop_at_first_error $[$
cmds: ?m.10593
cmds
]*) => do for
cmd: ?m.10736
cmd
in
cmds: Array (TSyntax `command)
cmds
do
elabCommand: Syntax → CommandElabM Unit
elabCommand
cmd: ?m.10736
cmd
.
raw: {ks : SyntaxNodeKinds} → TSyntax ks → Syntax
raw
if
(← get): ?m.11002
(←
get: {σ : outParam (Type ?u.10824)} → {m : Type ?u.10824 → Type ?u.10823} → [self : MonadState σ m] → m σ
get
(← get): ?m.11002
)
.
messages: State → MessageLog
messages
.
hasErrors: MessageLog → Bool
hasErrors
then
break: ?m.11099 ?m.11101
break
syntax
irredDefLemma: ParserDescr
irredDefLemma
:= atomic("(" "lemma" " := ") ident ")" /-- Introduces an irreducible definition. `irreducible_def foo := 42` generates a constant `foo : Nat` as well as a theorem `foo_def : foo = 42`. -/ elab
mods: ?m.13480
mods
:
declModifiers: Parser.Parser
declModifiers
"irreducible_def"
n_id: ?m.13470
n_id
:declId
n_def: ?m.13456
n_def
:(
irredDefLemma: ParserDescr
irredDefLemma
)?
declSig: ?m.13449
declSig
:
optDeclSig: Parser.Parser
optDeclSig
val: ?m.13440
val
:
declVal: Parser.Parser
declVal
: command => do let (
n: TSyntax `ident
n
,
us: Option (Syntax.TSepArray `ident ",")
us
) ← match
n_id: ?m.13470
n_id
with | `(
Parser.Command.declId: Parser.Parser
Parser.Command.declId
| $
n: ?m.13992
n
:ident $[.{$
us: ?m.13654 x✝
us
,*}]?) =>
pure: {f : Type ?u.14035 → Type ?u.14034} → [self : Pure f] → {α : Type ?u.14035} → α → f α
pure
pure (n, us): CommandElabM (?m.13516 y✝)
(
n: ?m.13992
n
pure (n, us): CommandElabM (?m.13516 y✝)
,
us: ?m.13654 x✝
us
pure (n, us): CommandElabM (?m.13516 y✝)
)
| _ =>
throwUnsupportedSyntax: CommandElabM (?m.13516 y✝)
throwUnsupportedSyntax
let
us': ?m.14406
us'
:=
us: Option (Syntax.TSepArray `ident ",")
us
.
getD: {α : Type ?u.14407} → Option α → α → α
getD
{ elemsAndSeps :=
#[]: Array ?m.14415
#[]
} let
n_def: ?m.14421
n_def
← match
n_def: ?m.13456
n_def
.
getD: {α : Type ?u.14650} → Option α → α → α
getD
⟨
mkNullNode: optParam (Array Syntax) #[] → Syntax
mkNullNode
⟩ with | `(
irredDefLemma: ParserDescr
irredDefLemma
| (lemma := $
id: ?m.14558
id
)) =>
pure: {f : Type ?u.14601 → Type ?u.14600} → [self : Pure f] → {α : Type ?u.14601} → α → f α
pure
pure id: CommandElabM (?m.14425 y✝)
id: ?m.14558
id
| _ =>
pure: {f : Type ?u.14696 → Type ?u.14695} → [self : Pure f] → {α : Type ?u.14696} → α → f α
pure
pure <| mkIdent <| (·.review) <| let scopes := extractMacroScopes n.getId { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
<|
mkIdent: Name → Ident
mkIdent
pure <| mkIdent <| (·.review) <| let scopes := extractMacroScopes n.getId { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
<| (·.
review: MacroScopesView → Name
review
pure <| mkIdent <| (·.review) <| let scopes := extractMacroScopes n.getId { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
) <|
pure <| mkIdent <| (·.review) <| let scopes := extractMacroScopes n.getId { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
let
pure <| mkIdent <| (·.review) <| let scopes := extractMacroScopes n.getId { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
scopes: ?m.14730
scopes
pure <| mkIdent <| (·.review) <| let scopes := extractMacroScopes n.getId { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
:=
extractMacroScopes: Name → MacroScopesView
extractMacroScopes
pure <| mkIdent <| (·.review) <| let scopes := extractMacroScopes n.getId { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
n: TSyntax `ident
n
pure <| mkIdent <| (·.review) <| let scopes := extractMacroScopes n.getId { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
.
getId: Ident → Name
getId
pure <| mkIdent <| (·.review) <| let scopes := extractMacroScopes n.getId { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
{
scopes: ?m.14730
scopes
pure <| mkIdent <| (·.review) <| let scopes := extractMacroScopes n.getId { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
pure <| mkIdent <| (·.review) <| let scopes := extractMacroScopes n.getId { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
with
pure <| mkIdent <| (·.review) <| let scopes := extractMacroScopes n.getId { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
name
pure <| mkIdent <| (·.review) <| let scopes := extractMacroScopes n.getId { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
:=
scopes: ?m.14730
scopes
pure <| mkIdent <| (·.review) <| let scopes := extractMacroScopes n.getId { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
.
name: MacroScopesView → Name
name
pure <| mkIdent <| (·.review) <| let scopes := extractMacroScopes n.getId { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
.
appendAfter: Name → String → Name
appendAfter
pure <| mkIdent <| (·.review) <| let scopes := extractMacroScopes n.getId { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
"_def": String
"_def"
pure <| mkIdent <| (·.review) <| let scopes := extractMacroScopes n.getId { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
}
let `(
Parser.Command.declModifiersF: Parser.Parser
Parser.Command.declModifiersF
| $[$
doc: ?m.14884
doc
:
docComment: Parser.Parser
docComment
]? $[@[$
attrs: ?m.15427 x✝
attrs
,*]]? $[$
vis: ?m.16015
vis
]? $[$
nc: ?m.16205
nc
:
noncomputable: Parser.Parser
noncomputable
]? $[$
uns: ?m.16743
uns
:unsafe]?) :=
mods: ?m.13480
mods
| throwError "unsupported modifiers {
format: {α : Type ?u.20628} → [self : ToFormat α] → α → Format
format
mods: ?m.13480
mods
}" let
attrs: ?m.17059
attrs
:=
attrs: ?m.15427 x✝³
attrs
.
getD: {α : Type ?u.17060} → Option α → α → α
getD
{}: ?m.17066
{}
let
prot: ?m.17111
prot
:=
vis: ?m.15914 x✝²
vis
.
filter: {α : Type ?u.17112} → (α → Bool) → Option α → Option α
filter
(· matches `(
Parser.Command.visibility: Parser.Parser
Parser.Command.visibility
| protected)) let
priv: ?m.17272
priv
:=
vis: ?m.15914 x✝²
vis
.
filter: {α : Type ?u.17273} → (α → Bool) → Option α → Option α
filter
(· matches `(
Parser.Command.visibility: Parser.Parser
Parser.Command.visibility
| private))
elabCommand: Syntax → CommandElabM Unit
elabCommand
<|<- `(stop_at_first_error $[$
nc: ?m.16209 x✝¹
nc
:
noncomputable: Parser.Parser
noncomputable
]? $[$
uns: TSyntax `Lean.Parser.Command.unsafe
uns
]? def definition$[.{$
us: Option (Syntax.TSepArray `ident ",")
us
,*}]? $
declSig: ?m.13449
declSig
:
optDeclSig: Parser.Parser
optDeclSig
$
val: ?m.13440
val
$[$
nc: ?m.16209 x✝¹
nc
:
noncomputable: Parser.Parser
noncomputable
]? $[$
uns: TSyntax `Lean.Parser.Command.unsafe
uns
]? opaque wrapped$[.{$
us: Option (Syntax.TSepArray `ident ",")
us
,*}]? : Subtype (Eq @definition.{$
us': ?m.14406
us'
,*}) := ⟨_, rfl⟩ $[$
doc: ?m.14888 x✝⁴
doc
:
docComment: Parser.Parser
docComment
]? $[private%$
priv: ?m.17272
priv
]? $[$
nc: TSyntax `Lean.Parser.Command.noncomputable
nc
:
noncomputable: Parser.Parser
noncomputable
]? $[$
uns: ?m.16640 x✝
uns
]? def $
n: TSyntax `ident
n
:ident$[.{$
us: Option (Syntax.TSepArray `ident ",")
us
,*}]? := val_proj @wrapped.{$
us': ?m.14406
us'
,*} $[private%$
priv: Syntax
priv
]? $[$
uns: TSyntax `Lean.Parser.Command.unsafe
uns
:unsafe]? theorem $
n_def: ?m.14421
n_def
:ident $[.{$
us: Option (Syntax.TSepArray `ident ",")
us
,*}]? : eta_helper Eq @$
n: TSyntax `ident
n
.{$
us': ?m.14406
us'
,*} @(delta% @definition) := by intros delta $
n: TSyntax `ident
n
:ident rw [show wrapped = ⟨@definition.{$
us': ?m.14406
us'
,*}, rfl⟩ from Subtype.ext wrapped.2.symm] rfl attribute [irreducible] $
n: TSyntax `ident
n
definition attribute [eqns $
n_def: ?m.14421
n_def
] $
n: TSyntax `ident
n
attribute [$
attrs: ?m.17059
attrs
:attrInstance,*] $
n: TSyntax `ident
n
) if
prot: ?m.17111
prot
.
isSome: {α : Type ?u.19979} → Option α → Bool
isSome
then
modifyEnv: {m : Type → Type} → [self : MonadEnv m] → (Environment → Environment) → m Unit
modifyEnv
(
addProtected: Environment → Name → Environment
addProtected
· ((←
getCurrNamespace: {m : Type → Type} → [self : MonadResolveName m] → m Name
getCurrNamespace
) ++
n: TSyntax `ident
n
.
getId: Ident → Name
getId
))