doc: relocate doc strings from elab to syntax
This commit is contained in:
Mario Carneiro
Leonardo de Moura
parent
b0db7deeef
commit
014db5d6d0
11 changed files with 147 additions and 116 deletions
|
|
@ -1396,12 +1396,9 @@ private def elabAtom : TermElab := fun stx expectedType? => do
|
|||
annotateIfRec stx (← elabAppAux stx #[] #[] (ellipsis := false) expectedType?)
|
||||
|
||||
@[builtinTermElab ident] def elabIdent : TermElab := elabAtom
|
||||
/-- `x@e` matches the pattern `e` and binds its value to the identifier `x`. -/
|
||||
@[builtinTermElab namedPattern] def elabNamedPattern : TermElab := elabAtom
|
||||
@[builtinTermElab dotIdent] def elabDotIdent : TermElab := elabAtom
|
||||
/-- `x.{u, ...}` explicitly specifies the universes `u, ...` of the constant `x`. -/
|
||||
@[builtinTermElab explicitUniv] def elabExplicitUniv : TermElab := elabAtom
|
||||
/-- `e |>.x` is a shorthand for `(e).x`. It is especially useful for avoiding parentheses with repeated applications. -/
|
||||
@[builtinTermElab pipeProj] def elabPipeProj : TermElab
|
||||
| `($e |>.$f $args*), expectedType? =>
|
||||
universeConstraintsCheckpoint do
|
||||
|
|
@ -1409,9 +1406,6 @@ private def elabAtom : TermElab := fun stx expectedType? => do
|
|||
elabAppAux (← `($e |>.$f)) namedArgs args (ellipsis := ellipsis) expectedType?
|
||||
| _, _ => throwUnsupportedSyntax
|
||||
|
||||
/--
|
||||
`@x` disables automatic insertion of implicit parameters of the constant `x`.
|
||||
`@e` for any term `e` also disables the insertion of implicit lambdas at this position. -/
|
||||
@[builtinTermElab explicit] def elabExplicit : TermElab := fun stx expectedType? =>
|
||||
match stx with
|
||||
| `(@$_:ident) => elabAtom stx expectedType? -- Recall that `elabApp` also has support for `@`
|
||||
|
|
|
|||
|
|
@ -26,12 +26,6 @@ open Meta
|
|||
mkCoe expectedType type e
|
||||
| _ => throwError "invalid coercion notation, expected type is not known"
|
||||
|
||||
/--
|
||||
The *anonymous constructor* `⟨e, ...⟩` is equivalent to `c e ...` if the
|
||||
expected type is an inductive type with a single constructor `c`.
|
||||
If more terms are given than `c` has parameters, the remaining arguments
|
||||
are turned into a new anonymous constructor application. For example,
|
||||
`⟨a, b, c⟩ : α × (β × γ)` is equivalent to `⟨a, ⟨b, c⟩⟩`. -/
|
||||
@[builtinTermElab anonymousCtor] def elabAnonymousCtor : TermElab := fun stx expectedType? =>
|
||||
match stx with
|
||||
| `(⟨$args,*⟩) => do
|
||||
|
|
@ -123,13 +117,6 @@ private def elabTParserMacroAux (prec lhsPrec e : Term) : TermElabM Syntax := do
|
|||
elabTParserMacroAux (prec?.getD <| quote Parser.maxPrec) (lhsPrec?.getD <| quote 0) e
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
/--
|
||||
`panic! msg` formally evaluates to `@Inhabited.default α` if the expected type
|
||||
`α` implements `Inhabited`.
|
||||
At runtime, `msg` and the file position are printed to stderr unless the C
|
||||
function `lean_set_panic_messages(false)` has been executed before. If the C
|
||||
function `lean_set_exit_on_panic(true)` has been executed before, the process is
|
||||
then aborted. -/
|
||||
@[builtinTermElab Lean.Parser.Term.panic] def elabPanic : TermElab := fun stx expectedType? => do
|
||||
match stx with
|
||||
| `(panic! $arg) =>
|
||||
|
|
@ -141,11 +128,9 @@ then aborted. -/
|
|||
withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
/-- A shorthand for `panic! "unreachable code has been reached"`. -/
|
||||
@[builtinMacro Lean.Parser.Term.unreachable] def expandUnreachable : Macro := fun _ =>
|
||||
`(panic! "unreachable code has been reached")
|
||||
|
||||
/-- `assert! cond` panics if `cond` evaluates to `false`. -/
|
||||
@[builtinMacro Lean.Parser.Term.assert] def expandAssert : Macro
|
||||
| `(assert! $cond; $body) =>
|
||||
-- TODO: support for disabling runtime assertions
|
||||
|
|
@ -154,15 +139,11 @@ then aborted. -/
|
|||
| none => `(if $cond then $body else panic! ("assertion violation"))
|
||||
| _ => Macro.throwUnsupported
|
||||
|
||||
/--
|
||||
`dbg_trace e; body` evaluates to `body` and prints `e` (which can be an
|
||||
interpolated string literal) to stderr. It should only be used for debugging. -/
|
||||
@[builtinMacro Lean.Parser.Term.dbgTrace] def expandDbgTrace : Macro
|
||||
| `(dbg_trace $arg:interpolatedStr; $body) => `(dbgTrace (s! $arg) fun _ => $body)
|
||||
| `(dbg_trace $arg:term; $body) => `(dbgTrace (toString $arg) fun _ => $body)
|
||||
| _ => Macro.throwUnsupported
|
||||
|
||||
/-- A temporary placeholder for a missing proof or value. -/
|
||||
@[builtinTermElab «sorry»] def elabSorry : TermElab := fun stx expectedType? => do
|
||||
let stxNew ← `(sorryAx _ false)
|
||||
withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
|
||||
|
|
@ -241,19 +222,6 @@ where
|
|||
| `(($e)) => Term.expandCDot? e
|
||||
| _ => Term.expandCDot? stx
|
||||
|
||||
|
||||
/--
|
||||
You can use parentheses for
|
||||
- Grouping expressions, e.g., `a * (b + c)`.
|
||||
- Creating tuples, e.g., `(a, b, c)` is notation for `Prod.mk a (Prod.mk b c)`.
|
||||
- Performing type ascription, e.g., `(0 : Int)` instructs Lean to process `0` as a value of type `Int`.
|
||||
- Creating `Unit.unit`, `()` is just a shorthand for `Unit.unit`.
|
||||
- Creating simple functions when combined with `·`. Here are some examples:
|
||||
- `(· + 1)` is shorthand for `fun x => x + 1`
|
||||
- `(· + ·)` is shorthand for `fun x y => x + y`
|
||||
- `(f · a b)` is shorthand for `fun x => f x a b`
|
||||
- `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x`
|
||||
-/
|
||||
@[builtinMacro Lean.Parser.Term.paren] def expandParen : Macro
|
||||
| `(()) => `(Unit.unit)
|
||||
| `(($e : $type)) => do
|
||||
|
|
@ -298,12 +266,6 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex
|
|||
let aux ← withLocalDeclD id (← inferType e) fun x => do mkLambdaFVars #[x] (← k (mkIdentFrom stx id))
|
||||
return mkApp aux e
|
||||
|
||||
/--
|
||||
`h ▸ e` is a macro built on top of `Eq.rec` and `Eq.symm` definitions.
|
||||
Given `h : a = b` and `e : p a`, the term `h ▸ e` has type `p b`.
|
||||
You can also view `h ▸ e` as a "type casting" operation where you change the type of `e` by using `h`.
|
||||
See the Chapter "Quantifiers and Equality" in the manual "Theorem Proving in Lean" for additional information.
|
||||
-/
|
||||
@[builtinTermElab subst] def elabSubst : TermElab := fun stx expectedType? => do
|
||||
let expectedType? ← tryPostponeIfHasMVars? expectedType?
|
||||
match stx with
|
||||
|
|
|
|||
|
|
@ -9,7 +9,6 @@ import Lean.Elab.Eval
|
|||
namespace Lean.Elab.Term
|
||||
open Meta
|
||||
|
||||
/-- The universe of propositions. `Prop ≡ Sort 0`. -/
|
||||
@[builtinTermElab «prop»] def elabProp : TermElab := fun _ _ =>
|
||||
return mkSort levelZero
|
||||
|
||||
|
|
@ -19,11 +18,9 @@ private def elabOptLevel (stx : Syntax) : TermElabM Level :=
|
|||
else
|
||||
elabLevel stx[0]
|
||||
|
||||
/-- A specific universe in Lean's infinite hierarchy of universes. -/
|
||||
@[builtinTermElab «sort»] def elabSort : TermElab := fun stx _ =>
|
||||
return mkSort (← elabOptLevel stx[1])
|
||||
|
||||
/-- A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. -/
|
||||
@[builtinTermElab «type»] def elabTypeStx : TermElab := fun stx _ =>
|
||||
return mkSort (mkLevelSucc (← elabOptLevel stx[1]))
|
||||
|
||||
|
|
@ -56,7 +53,6 @@ private def elabOptLevel (stx : Syntax) : TermElabM Level :=
|
|||
else
|
||||
elabPipeCompletion stx expectedType?
|
||||
|
||||
/-- A placeholder term, to be synthesized by unification. -/
|
||||
@[builtinTermElab «hole»] def elabHole : TermElab := fun stx expectedType? => do
|
||||
let mvar ← mkFreshExprMVar expectedType?
|
||||
registerMVarErrorHoleInfo mvar.mvarId! stx
|
||||
|
|
@ -149,7 +145,6 @@ private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr :=
|
|||
registerSyntheticMVar ref mvarId <| SyntheticMVarKind.tactic tacticCode (← saveContext)
|
||||
return mvar
|
||||
|
||||
/-- `by tac` constructs a term of the expected type by running the tactic(s) `tac`. -/
|
||||
@[builtinTermElab byTactic] def elabByTactic : TermElab := fun stx expectedType? => do
|
||||
match expectedType? with
|
||||
| some expectedType => mkTacticMVar expectedType stx
|
||||
|
|
@ -208,30 +203,19 @@ def elabScientificLit : TermElab := fun stx expectedType? => do
|
|||
| some val => return mkApp (Lean.mkConst ``Char.ofNat) (mkRawNatLit val.toNat)
|
||||
| none => throwIllFormedSyntax
|
||||
|
||||
/-- A literal of type `Name`. -/
|
||||
@[builtinTermElab quotedName] def elabQuotedName : TermElab := fun stx _ =>
|
||||
match stx[0].isNameLit? with
|
||||
| some val => pure $ toExpr val
|
||||
| none => throwIllFormedSyntax
|
||||
|
||||
/--
|
||||
A resolved name literal. Evaluates to the full name of the given constant if
|
||||
existent in the current context, or else fails. -/
|
||||
@[builtinTermElab doubleQuotedName] def elabDoubleQuotedName : TermElab := fun stx _ =>
|
||||
return toExpr (← resolveGlobalConstNoOverloadWithInfo stx[2])
|
||||
|
||||
/-- A macro which evaluates to the name of the currently elaborating declaration. -/
|
||||
@[builtinTermElab declName] def elabDeclName : TermElab := adaptExpander fun _ => do
|
||||
let some declName ← getDeclName?
|
||||
| throwError "invalid `decl_name%` macro, the declaration name is not available"
|
||||
return (quote declName : Term)
|
||||
|
||||
/--
|
||||
* `with_decl_name% id e` elaborates `e` in a context while changing the effective
|
||||
declaration name to `id`.
|
||||
* `with_decl_name% ? id e` does the same, but resolves `id` as a new definition name
|
||||
(appending the current namespaces).
|
||||
-/
|
||||
@[builtinTermElab Parser.Term.withDeclName] def elabWithDeclName : TermElab := fun stx expectedType? => do
|
||||
let id := stx[2].getId
|
||||
let id := if stx[1].isNone then id else (← getCurrNamespace) ++ id
|
||||
|
|
@ -283,7 +267,6 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
|
|||
| none => throwIllFormedSyntax
|
||||
| some msg => elabTermEnsuringType stx[2] expectedType? (errorMsgHeader? := msg)
|
||||
|
||||
/-- `open ... in e` makes the given namespaces available in the term `e`. -/
|
||||
@[builtinTermElab «open»] def elabOpen : TermElab := fun stx expectedType? => do
|
||||
try
|
||||
pushScope
|
||||
|
|
@ -293,7 +276,6 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
|
|||
finally
|
||||
popScope
|
||||
|
||||
/-- `set_option opt val in e` sets the option `opt` to the value `val` in the term `e`. -/
|
||||
@[builtinTermElab «set_option»] def elabSetOption : TermElab := fun stx expectedType? => do
|
||||
let options ← Elab.elabSetOption stx[1] stx[2]
|
||||
withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do
|
||||
|
|
|
|||
|
|
@ -1245,15 +1245,6 @@ where
|
|||
isAtomicIdent (stx : Syntax) : Bool :=
|
||||
stx.isIdent && stx.getId.eraseMacroScopes.isAtomic
|
||||
|
||||
/--
|
||||
Pattern matching. `match e, ... with | p, ... => f | ...` matches each given
|
||||
term `e` against each pattern `p` of a match alternative. When all patterns
|
||||
of an alternative match, the `match` term evaluates to the value of the
|
||||
corresponding right-hand side `f` with the pattern variables bound to the
|
||||
respective matched values.
|
||||
When not constructing a proof, `match` does not automatically substitute variables
|
||||
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
|
||||
enforce this. -/
|
||||
@[builtinTermElab «match»] def elabMatch : TermElab := fun stx expectedType? => do
|
||||
match stx with
|
||||
| `(match $discr:term with | $y:ident => $rhs) =>
|
||||
|
|
@ -1277,9 +1268,6 @@ builtin_initialize
|
|||
registerTraceClass `Elab.match
|
||||
|
||||
-- leading_parser:leadPrec "nomatch " >> termParser
|
||||
/-- Empty match/ex falso. `nomatch e` is of arbitrary type `α : Sort u` if
|
||||
Lean can show that an empty set of patterns is exhaustive given `e`'s type,
|
||||
e.g. because it has no constructors. -/
|
||||
@[builtinTermElab «nomatch»] def elabNoMatch : TermElab := fun stx expectedType? => do
|
||||
match stx with
|
||||
| `(nomatch $discrExpr) =>
|
||||
|
|
|
|||
|
|
@ -649,23 +649,6 @@ def match_syntax.expand (stx : Syntax) : TermElabM Syntax := do
|
|||
return stx
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
/--
|
||||
Syntactic pattern match. Matches a `Syntax` value against quotations, pattern variables, or `_`.
|
||||
|
||||
Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly.
|
||||
|
||||
`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
|
||||
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching.
|
||||
For example, in
|
||||
```lean
|
||||
syntax "c" ("foo" <|> "bar") ...
|
||||
```
|
||||
`foo` and `bar` are indistinguishable during matching, but in
|
||||
```lean
|
||||
syntax foo := "foo"
|
||||
syntax "c" (foo <|> "bar") ...
|
||||
```
|
||||
they are not. -/
|
||||
@[builtinTermElab «match»] def elabMatchSyntax : TermElab :=
|
||||
adaptExpander match_syntax.expand
|
||||
|
||||
|
|
|
|||
|
|
@ -15,7 +15,7 @@ open Std (HashMap)
|
|||
open Meta
|
||||
open TSyntax.Compat
|
||||
|
||||
/--
|
||||
/-
|
||||
Structure instances are of the form:
|
||||
|
||||
"{" >> optional (atomic (sepBy1 termParser ", " >> " with "))
|
||||
|
|
@ -896,13 +896,6 @@ private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (sour
|
|||
synthesizeAppInstMVars instMVars r
|
||||
return r
|
||||
|
||||
/-- Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
|
||||
inherited. If `e` is itself a variable called `x`, it can be elided:
|
||||
`fun y => { x := 1, y }`.
|
||||
A *structure update* of an existing value can be given via `with`:
|
||||
`{ point with x := 1 }`.
|
||||
The structure type can be specified if not inferable:
|
||||
`{ x := 1, y := 2 : Point }`. -/
|
||||
@[builtinTermElab structInst] def elabStructInst : TermElab := fun stx expectedType? => do
|
||||
match (← expandNonAtomicExplicitSources stx) with
|
||||
| some stxNew => withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
|
||||
|
|
|
|||
|
|
@ -176,11 +176,17 @@ builtin_initialize
|
|||
end Command
|
||||
|
||||
namespace Term
|
||||
/-- `open Foo in e` is like `open Foo` but scoped to a single term. -/
|
||||
/--
|
||||
`open Foo in e` is like `open Foo` but scoped to a single term.
|
||||
It makes the given namespaces available in the term `e`.
|
||||
-/
|
||||
@[builtinTermParser] def «open» := leading_parser:leadPrec
|
||||
"open " >> Command.openDecl >> withOpenDecl (" in " >> termParser)
|
||||
|
||||
/-- `set_option opt val in e` is like `set_option opt val` but scoped to a single term. -/
|
||||
/--
|
||||
`set_option opt val in e` is like `set_option opt val` but scoped to a single term.
|
||||
It sets the option `opt` to the value `val` in the term `e`.
|
||||
-/
|
||||
@[builtinTermParser] def «set_option» := leading_parser:leadPrec
|
||||
"set_option " >> ident >> ppSpace >> Command.optionValue >> " in " >> termParser
|
||||
end Term
|
||||
|
|
|
|||
|
|
@ -53,6 +53,7 @@ namespace Term
|
|||
|
||||
/-! # Built-in parsers -/
|
||||
|
||||
/-- `by tac` constructs a term of the expected type by running the tactic(s) `tac`. -/
|
||||
@[builtinTermParser] def byTactic := leading_parser:leadPrec ppAllowUngrouped >> "by " >> Tactic.tacticSeq
|
||||
|
||||
/--
|
||||
|
|
@ -72,17 +73,41 @@ def optSemicolon (p : Parser) : Parser := ppDedent $ semicolonOrLinebreak >> ppL
|
|||
@[builtinTermParser] def scientific : Parser := checkPrec maxPrec >> scientificLit
|
||||
@[builtinTermParser] def str : Parser := checkPrec maxPrec >> strLit
|
||||
@[builtinTermParser] def char : Parser := checkPrec maxPrec >> charLit
|
||||
/-- A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. -/
|
||||
@[builtinTermParser] def type := leading_parser "Type" >> optional (checkWsBefore "" >> checkPrec leadPrec >> checkColGt >> levelParser maxPrec)
|
||||
/-- A specific universe in Lean's infinite hierarchy of universes. -/
|
||||
@[builtinTermParser] def sort := leading_parser "Sort" >> optional (checkWsBefore "" >> checkPrec leadPrec >> checkColGt >> levelParser maxPrec)
|
||||
/-- The universe of propositions. `Prop ≡ Sort 0`. -/
|
||||
@[builtinTermParser] def prop := leading_parser "Prop"
|
||||
/-- A placeholder term, to be synthesized by unification. -/
|
||||
@[builtinTermParser] def hole := leading_parser "_"
|
||||
@[builtinTermParser] def syntheticHole := leading_parser "?" >> (ident <|> hole)
|
||||
/-- A temporary placeholder for a missing proof or value. -/
|
||||
@[builtinTermParser] def «sorry» := leading_parser "sorry"
|
||||
@[builtinTermParser] def cdot := leading_parser symbol "·" <|> "."
|
||||
def typeAscription := leading_parser " : " >> termParser
|
||||
def tupleTail := leading_parser ", " >> sepBy1 termParser ", "
|
||||
def parenSpecial : Parser := optional (tupleTail <|> typeAscription)
|
||||
/--
|
||||
You can use parentheses for
|
||||
- Grouping expressions, e.g., `a * (b + c)`.
|
||||
- Creating tuples, e.g., `(a, b, c)` is notation for `Prod.mk a (Prod.mk b c)`.
|
||||
- Performing type ascription, e.g., `(0 : Int)` instructs Lean to process `0` as a value of type `Int`.
|
||||
- Creating `Unit.unit`, `()` is just a shorthand for `Unit.unit`.
|
||||
- Creating simple functions when combined with `·`. Here are some examples:
|
||||
- `(· + 1)` is shorthand for `fun x => x + 1`
|
||||
- `(· + ·)` is shorthand for `fun x y => x + y`
|
||||
- `(f · a b)` is shorthand for `fun x => f x a b`
|
||||
- `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x`
|
||||
-/
|
||||
@[builtinTermParser] def paren := leading_parser "(" >> (withoutPosition (withoutForbidden (optional (ppDedentIfGrouped termParser >> parenSpecial)))) >> ")"
|
||||
/--
|
||||
The *anonymous constructor* `⟨e, ...⟩` is equivalent to `c e ...` if the
|
||||
expected type is an inductive type with a single constructor `c`.
|
||||
If more terms are given than `c` has parameters, the remaining arguments
|
||||
are turned into a new anonymous constructor application. For example,
|
||||
`⟨a, b, c⟩ : α × (β × γ)` is equivalent to `⟨a, ⟨b, c⟩⟩`.
|
||||
-/
|
||||
@[builtinTermParser] def anonymousCtor := leading_parser "⟨" >> sepBy termParser ", " >> "⟩"
|
||||
def optIdent : Parser := optional (atomic (ident >> " : "))
|
||||
def fromTerm := leading_parser "from " >> termParser
|
||||
|
|
@ -95,12 +120,25 @@ def structInstLVal := leading_parser (ident <|> fieldIdx <|> structInstArrayRe
|
|||
def structInstField := ppGroup $ leading_parser structInstLVal >> " := " >> termParser
|
||||
def structInstFieldAbbrev := leading_parser atomic (ident >> notFollowedBy ("." <|> ":=" <|> symbol "[") "invalid field abbreviation") -- `x` is an abbreviation for `x := x`
|
||||
def optEllipsis := leading_parser optional ".."
|
||||
/--
|
||||
Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
|
||||
inherited. If `e` is itself a variable called `x`, it can be elided:
|
||||
`fun y => { x := 1, y }`.
|
||||
A *structure update* of an existing value can be given via `with`:
|
||||
`{ point with x := 1 }`.
|
||||
The structure type can be specified if not inferable:
|
||||
`{ x := 1, y := 2 : Point }`.
|
||||
-/
|
||||
@[builtinTermParser] def structInst := leading_parser "{" >> ppHardSpace >> optional (atomic (sepBy1 termParser ", " >> " with "))
|
||||
>> sepByIndent (structInstFieldAbbrev <|> structInstField) ", " (allowTrailingSep := true)
|
||||
>> optEllipsis
|
||||
>> optional (" : " >> termParser) >> " }"
|
||||
def typeSpec := leading_parser " : " >> termParser
|
||||
def optType : Parser := optional typeSpec
|
||||
/--
|
||||
`@x` disables automatic insertion of implicit parameters of the constant `x`.
|
||||
`@e` for any term `e` also disables the insertion of implicit lambdas at this position.
|
||||
-/
|
||||
@[builtinTermParser] def explicit := leading_parser "@" >> termParser maxPrec
|
||||
@[builtinTermParser] def inaccessible := leading_parser ".(" >> termParser >> ")"
|
||||
def binderIdent : Parser := ident <|> hole
|
||||
|
|
@ -158,7 +196,42 @@ def generalizingParam := leading_parser atomic ("(" >> nonReservedSymbol "genera
|
|||
|
||||
def motive := leading_parser atomic ("(" >> nonReservedSymbol "motive" >> " := ") >> termParser >> ")" >> ppSpace
|
||||
|
||||
/--
|
||||
Pattern matching. `match e, ... with | p, ... => f | ...` matches each given
|
||||
term `e` against each pattern `p` of a match alternative. When all patterns
|
||||
of an alternative match, the `match` term evaluates to the value of the
|
||||
corresponding right-hand side `f` with the pattern variables bound to the
|
||||
respective matched values.
|
||||
When not constructing a proof, `match` does not automatically substitute variables
|
||||
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
|
||||
enforce this.
|
||||
|
||||
Syntax quotations can also be used in a pattern match.
|
||||
This matches a `Syntax` value against quotations, pattern variables, or `_`.
|
||||
|
||||
Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
|
||||
names only should be done explicitly.
|
||||
|
||||
`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
|
||||
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
|
||||
should participate in matching.
|
||||
For example, in
|
||||
```lean
|
||||
syntax "c" ("foo" <|> "bar") ...
|
||||
```
|
||||
`foo` and `bar` are indistinguishable during matching, but in
|
||||
```lean
|
||||
syntax foo := "foo"
|
||||
syntax "c" (foo <|> "bar") ...
|
||||
```
|
||||
they are not.
|
||||
-/
|
||||
@[builtinTermParser] def «match» := leading_parser:leadPrec "match " >> optional generalizingParam >> optional motive >> sepBy1 matchDiscr ", " >> " with " >> ppDedent matchAlts
|
||||
/--
|
||||
Empty match/ex falso. `nomatch e` is of arbitrary type `α : Sort u` if
|
||||
Lean can show that an empty set of patterns is exhaustive given `e`'s type,
|
||||
e.g. because it has no constructors.
|
||||
-/
|
||||
@[builtinTermParser] def «nomatch» := leading_parser:leadPrec "nomatch " >> termParser
|
||||
|
||||
def funImplicitBinder := withAntiquot (mkAntiquot "implicitBinder" ``implicitBinder) <| atomic (lookahead ("{" >> many1 binderIdent >> (symbol " : " <|> "}"))) >> implicitBinder
|
||||
|
|
@ -174,7 +247,12 @@ def withAnonymousAntiquot := leading_parser atomic ("(" >> nonReservedSymbol "wi
|
|||
@[builtinTermParser] def «trailing_parser» := leading_parser:leadPrec "trailing_parser " >> optExprPrecedence >> optExprPrecedence >> termParser
|
||||
|
||||
@[builtinTermParser] def borrowed := leading_parser "@& " >> termParser leadPrec
|
||||
/-- A literal of type `Name`. -/
|
||||
@[builtinTermParser] def quotedName := leading_parser nameLit
|
||||
/--
|
||||
A resolved name literal. Evaluates to the full name of the given constant if
|
||||
existent in the current context, or else fails.
|
||||
-/
|
||||
-- use `rawCh` because ``"`" >> ident`` overlaps with `nameLit`, with the latter being preferred by the tokenizer
|
||||
-- note that we cannot use ```"``"``` as a new token either because it would break `precheckedQuot`
|
||||
@[builtinTermParser] def doubleQuotedName := leading_parser "`" >> checkNoWsBefore >> rawCh '`' (trailingWs := false) >> ident
|
||||
|
|
@ -272,7 +350,14 @@ def matchAltsWhereDecls := leading_parser matchAlts >> optional whereDecls
|
|||
@[builtinTermParser] def forInMacro := leading_parser "for_in% " >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec
|
||||
@[builtinTermParser] def forInMacro' := leading_parser "for_in'% " >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec
|
||||
|
||||
/-- A macro which evaluates to the name of the currently elaborating declaration. -/
|
||||
@[builtinTermParser] def declName := leading_parser "decl_name%"
|
||||
/--
|
||||
* `with_decl_name% id e` elaborates `e` in a context while changing the effective
|
||||
declaration name to `id`.
|
||||
* `with_decl_name% ?id e` does the same, but resolves `id` as a new definition name
|
||||
(appending the current namespaces).
|
||||
-/
|
||||
@[builtinTermParser] def withDeclName := leading_parser "with_decl_name% " >> optional "?" >> ident >> termParser
|
||||
@[builtinTermParser] def typeOf := leading_parser "type_of% " >> termParser maxPrec
|
||||
@[builtinTermParser] def ensureTypeOf := leading_parser "ensure_type_of% " >> termParser maxPrec >> strLit >> termParser
|
||||
|
|
@ -311,12 +396,21 @@ def isIdent (stx : Syntax) : Bool :=
|
|||
-- antiquotations should also be allowed where an identifier is expected
|
||||
stx.isAntiquot || stx.isIdent
|
||||
|
||||
/-- `x.{u, ...}` explicitly specifies the universes `u, ...` of the constant `x`. -/
|
||||
@[builtinTermParser] def explicitUniv : TrailingParser := trailing_parser checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '.{'" >> ".{" >> sepBy1 levelParser ", " >> "}"
|
||||
/-- `x@e` matches the pattern `e` and binds its value to the identifier `x`. -/
|
||||
@[builtinTermParser] def namedPattern : TrailingParser := trailing_parser checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '@'" >> "@" >> optional (atomic (ident >> ":")) >> termParser maxPrec
|
||||
|
||||
/-- `e |>.x` is a shorthand for `(e).x`. It is especially useful for avoiding parentheses with repeated applications. -/
|
||||
@[builtinTermParser] def pipeProj := trailing_parser:minPrec " |>." >> checkNoWsBefore >> (fieldIdx <|> rawIdent) >> many argument
|
||||
@[builtinTermParser] def pipeCompletion := trailing_parser:minPrec " |>."
|
||||
|
||||
/--
|
||||
`h ▸ e` is a macro built on top of `Eq.rec` and `Eq.symm` definitions.
|
||||
Given `h : a = b` and `e : p a`, the term `h ▸ e` has type `p b`.
|
||||
You can also view `h ▸ e` as a "type casting" operation where you change the type of `e` by using `h`.
|
||||
See the Chapter "Quantifiers and Equality" in the manual "Theorem Proving in Lean" for additional information.
|
||||
-/
|
||||
@[builtinTermParser] def subst := trailing_parser:75 " ▸ " >> sepBy1 (termParser 75) " ▸ "
|
||||
|
||||
-- NOTE: Doesn't call `categoryParser` directly in contrast to most other "static" quotations, so call `evalInsideQuot` explicitly
|
||||
|
|
@ -326,9 +420,23 @@ def bracketedBinderF := bracketedBinder -- no default arg
|
|||
@[builtinTermParser] def matchDiscr.quot : Parser := leading_parser "`(matchDiscr|" >> incQuotDepth (evalInsideQuot ``matchDiscr matchDiscr) >> ")"
|
||||
@[builtinTermParser] def attr.quot : Parser := leading_parser "`(attr|" >> incQuotDepth attrParser >> ")"
|
||||
|
||||
/--
|
||||
`panic! msg` formally evaluates to `@Inhabited.default α` if the expected type
|
||||
`α` implements `Inhabited`.
|
||||
At runtime, `msg` and the file position are printed to stderr unless the C
|
||||
function `lean_set_panic_messages(false)` has been executed before. If the C
|
||||
function `lean_set_exit_on_panic(true)` has been executed before, the process is
|
||||
then aborted.
|
||||
-/
|
||||
@[builtinTermParser] def panic := leading_parser:leadPrec "panic! " >> termParser
|
||||
/-- A shorthand for `panic! "unreachable code has been reached"`. -/
|
||||
@[builtinTermParser] def unreachable := leading_parser:leadPrec "unreachable!"
|
||||
/--
|
||||
`dbg_trace e; body` evaluates to `body` and prints `e` (which can be an
|
||||
interpolated string literal) to stderr. It should only be used for debugging.
|
||||
-/
|
||||
@[builtinTermParser] def dbgTrace := leading_parser:leadPrec withPosition ("dbg_trace" >> ((interpolatedStr termParser) <|> termParser)) >> optSemicolon termParser
|
||||
/-- `assert! cond` panics if `cond` evaluates to `false`. -/
|
||||
@[builtinTermParser] def assert := leading_parser:leadPrec withPosition ("assert! " >> termParser) >> optSemicolon termParser
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -168,11 +168,9 @@ def saveWidgetInfo [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m] (widg
|
|||
}
|
||||
pushInfoLeaf info
|
||||
|
||||
/-! # Widget command
|
||||
|
||||
Use `#widget <widgetname> <props>` to display a widget.
|
||||
-/
|
||||
/-! # Widget command -/
|
||||
|
||||
/-- Use `#widget <widgetname> <props>` to display a widget. Useful for debugging widgets. -/
|
||||
syntax (name := widgetCmd) "#widget " ident term : command
|
||||
|
||||
open Lean Lean.Meta Lean.Elab Lean.Elab.Term in
|
||||
|
|
@ -184,7 +182,6 @@ private opaque evalJson (stx : Syntax) : TermElabM Json
|
|||
|
||||
open Elab Command in
|
||||
|
||||
/-- Use this to place a widget. Useful for debugging widgets. -/
|
||||
@[commandElab widgetCmd] def elabWidgetCmd : CommandElab := fun
|
||||
| stx@`(#widget $id:ident $props) => do
|
||||
let props : Json ← runTermElabM fun _ => evalJson props
|
||||
|
|
|
|||
|
|
@ -1,8 +1,8 @@
|
|||
some { range := { pos := { line := 149, column := 41 },
|
||||
some { range := { pos := { line := 134, column := 41 },
|
||||
charUtf16 := 41,
|
||||
endPos := { line := 155, column := 31 },
|
||||
endPos := { line := 140, column := 31 },
|
||||
endCharUtf16 := 31 },
|
||||
selectionRange := { pos := { line := 149, column := 45 },
|
||||
selectionRange := { pos := { line := 134, column := 45 },
|
||||
charUtf16 := 45,
|
||||
endPos := { line := 149, column := 57 },
|
||||
endPos := { line := 134, column := 57 },
|
||||
endCharUtf16 := 57 } }
|
||||
|
|
|
|||
|
|
@ -2,29 +2,47 @@
|
|||
"position": {"line": 1, "character": 5}}
|
||||
{"range":
|
||||
{"start": {"line": 1, "character": 5}, "end": {"line": 1, "character": 6}},
|
||||
"contents": {"value": "```lean\nNat\n```", "kind": "markdown"}}
|
||||
"contents":
|
||||
{"value":
|
||||
"```lean\nNat\n```\n***\nA placeholder term, to be synthesized by unification. ",
|
||||
"kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://hoverBinderUndescore.lean"},
|
||||
"position": {"line": 1, "character": 7}}
|
||||
{"range":
|
||||
{"start": {"line": 1, "character": 7}, "end": {"line": 1, "character": 8}},
|
||||
"contents": {"value": "```lean\nBool\n```", "kind": "markdown"}}
|
||||
"contents":
|
||||
{"value":
|
||||
"```lean\nBool\n```\n***\nA placeholder term, to be synthesized by unification. ",
|
||||
"kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://hoverBinderUndescore.lean"},
|
||||
"position": {"line": 6, "character": 6}}
|
||||
{"range":
|
||||
{"start": {"line": 6, "character": 6}, "end": {"line": 6, "character": 7}},
|
||||
"contents": {"value": "```lean\nNat\n```", "kind": "markdown"}}
|
||||
"contents":
|
||||
{"value":
|
||||
"```lean\nNat\n```\n***\nA placeholder term, to be synthesized by unification. ",
|
||||
"kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://hoverBinderUndescore.lean"},
|
||||
"position": {"line": 6, "character": 8}}
|
||||
{"range":
|
||||
{"start": {"line": 6, "character": 8}, "end": {"line": 6, "character": 9}},
|
||||
"contents": {"value": "```lean\nBool\n```", "kind": "markdown"}}
|
||||
"contents":
|
||||
{"value":
|
||||
"```lean\nBool\n```\n***\nA placeholder term, to be synthesized by unification. ",
|
||||
"kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://hoverBinderUndescore.lean"},
|
||||
"position": {"line": 11, "character": 6}}
|
||||
{"range":
|
||||
{"start": {"line": 11, "character": 6}, "end": {"line": 11, "character": 7}},
|
||||
"contents": {"value": "```lean\nNat\n```", "kind": "markdown"}}
|
||||
"contents":
|
||||
{"value":
|
||||
"```lean\nNat\n```\n***\nA placeholder term, to be synthesized by unification. ",
|
||||
"kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://hoverBinderUndescore.lean"},
|
||||
"position": {"line": 11, "character": 8}}
|
||||
{"range":
|
||||
{"start": {"line": 11, "character": 8}, "end": {"line": 11, "character": 9}},
|
||||
"contents": {"value": "```lean\nBool\n```", "kind": "markdown"}}
|
||||
"contents":
|
||||
{"value":
|
||||
"```lean\nBool\n```\n***\nA placeholder term, to be synthesized by unification. ",
|
||||
"kind": "markdown"}}
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue