This PR adds auto-completion for identifiers after `end`. It also fixes
a bug where completion in the whitespace after `set_option` would not
yield the full option list.
Closes#3885.
### Breaking changes
The `«end»` syntax is adjusted to take an `identWithPartialTrailingDot`
instead of an `ident`.
This PR introduces a `coinductive` keyword, that can be used to define
coinductive predicates via a syntax identical to the one for `inductive`
keyword. The machinery relies on the implementation of elaboration of
inductive types and extracts an endomap on the appropriate space of the
predicates from the definition that is then fed to the
`PartialFixpoint`. Upon elaborating definitions, all the constructors
are declared through automatically generated lemmas.
For example, infinite sequence of transitions in a relation, can be
given by the following:
```lean4
section
variable (α : Type)
coinductive infSeq (r : α → α → Prop) : α → Prop where
| step : r a b → infSeq r b → infSeq r a
/--
info: infSeq.coinduct (α : Type) (r : α → α → Prop) (pred : α → Prop) (hyp : ∀ (x : α), pred x → ∃ b, r x b ∧ pred b)
(x✝ : α) : pred x✝ → infSeq α r x✝
-/
#guard_msgs in
#check infSeq.coinduct
/--
info: infSeq.step (α : Type) (r : α → α → Prop) {a b : α} : r a b → infSeq α r b → infSeq α r a
-/
#guard_msgs in
#check infSeq.step
end
```
The machinery also supports `mutual` blocks, as well as mixing inductive
and coinductive predicate definitions:
```lean4
mutual
coinductive tick : Prop where
| mk : ¬tock → tick
inductive tock : Prop where
| mk : ¬tick → tock
end
/--
info: tick.mutual_induct (pred_1 pred_2 : Prop) (hyp_1 : pred_1 → pred_2 → False) (hyp_2 : (pred_1 → False) → pred_2) :
(pred_1 → tick) ∧ (tock → pred_2)
-/
#guard_msgs in
#check tick.mutual_induct
```
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This PR implements module docstrings in Verso syntax, as well as adding
a number of improvements and fixes to Verso docstrings in general. In
particular, they now have language server support and are parsed at
parse time rather than elaboration time, so the snapshot's syntax tree
includes the parsed documentation.
This PR refines and clarifies the `meta` phase distinction in the module
system.
* `meta import A` without `public` now has the clarified meaning of
"enable compile-time evaluation of declarations in or above `A` in the
current module, but not downstream". This is now checked statically by
enforcing that public meta defs, which therefore may be referenced from
outside, can only use public meta imports, and that global evaluating
attributes such as `@[term_parser]` can only be applied to public meta
defs.
* `meta def`s may no longer reference non-meta defs even when in the
same module. This clarifies the meta distinction as well as improves
locality of (new) error messages.
* parser references in `syntax` are now also properly tracked as meta
references.
* A `meta import` of an `import` now properly loads only the `.ir` of
the nested module for the purposes of execution instead of also making
its declarations available for general elaboration.
* `initialize` is now no longer being run on import under the module
system, which is now covered by `meta initialize`.
This PR makes the builtin Verso docstring elaborators bootstrap
correctly, adds the ability to postpone checks (which is necessary for
resolving forward references and bootstrapping issues), and fixes a
minor parser bug.
This PR modifies macros, which implement non-atomic definitions and
```$cmd1 in $cmd2``` syntax. These macros involve implicit scopes,
introduced through ```section``` and ```namespace``` commands. Since
sections or namespaces are designed to delimit local attributes, this
has led to unintuitive behaviour when applying local attributes to
definitions appearing in the above-mentioned contexts. This has been
causing the following examples to fail:
```lean4
axiom A : Prop
namespace ex1
open Nat in
@[local simp] axiom a : A ↔ True
example : A := by simp
end ex1
namespace ex2
@[local simp] axiom Foo.a : A ↔ True
example : A := by simp
end ex2
```
This PR adds an internal-only piece of syntax,
```InternalSyntax.end_local_scope```, that influences the
```ScopedEnvExtension.addLocalEntry``` used in implementing local
attributes, to avoid delimiting local entries in the current scope. This
command is used in the above-mentioned macros.
Closes [#9445](https://github.com/leanprover/lean4/issues/9445).
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This PR generates `.ctorIdx` functions for all inductive types, not just
enumeration types. This can be a building block for other constructions
(`BEq`, `noConfusion`) that are size-efficient even for large
inductives.
It also renames it from `.toCtorIdx` to `.ctorIdx`, which is the more
idiomatic naming.
The old name exists as an alias, with a deprecation attribute to be
added after the next
stage0 update.
These functions can arguably compiled down to a rather efficient tag
lookup, rather than a `case` statement. This is future work (but
hopefully near future).
For a fair number of basic types the compiler is not able to compile a
function using `casesOn` until further definitions have been defined.
This therefore (ab)uses the `genInjectivity` flag and
`gen_injective_theorems%` command to also control the generation of this
construct.
For (slightly) more efficient kernel reduction one could use `.rec`
rather than `.casesOn`. I did not do that yet, also because it
complicates compilation.
This PR allows for more fine-grained control over what derived instances
have exposed definitions under the module system: handlers should not
expose their implementation unless either the deriving item or a
surrounding section is marked with `@[expose]`. Built-in handlers to be
updated after a stage 0 update.
This PR registers a parser alias for `Lean.Parser.Command.visibility`.
This avoids having to import `Lean.Parser.Command` in simple command
macros that use visibilities.
This PR improves the delta deriving handler, giving it the ability to
process definitions with binders, as well as the ability to recursively
unfold definitions. Furthermore, delta deriving now tries all explicit
non-out-param arguments to a class, and it can handle "mixin" instance
arguments. The `deriving` syntax has been changed to accept general
terms, which makes it possible to derive specific instances with for
example `deriving OfNat _ 1` or `deriving Module R`. The class is
allowed to be a pi type, to add additional hypotheses; here is a Mathlib
example:
```lean
def Sym (α : Type*) (n : ℕ) :=
{ s : Multiset α // Multiset.card s = n }
deriving [DecidableEq α] → DecidableEq _
```
This underscore stands for where `Sym α n` may be inserted, which is
necessary when `→` is used. The `deriving instance` command can refer to
scoped variables when delta deriving as well. Breaking change: the
derived instance's name uses the `instance` command's name generator,
and the new instance is added to the current namespace.
This closes
[mathlib4#380](https://github.com/leanprover-community/mathlib4/issues/380).
This PR adds a feature where `structure` constructors can override the
inferred binder kinds of the type's parameters. In the following, the
`(p)` binder on `toLp` causes `p` to be an explicit parameter to
`WithLp.toLp`:
```lean
structure WithLp (p : Nat) (V : Type) where toLp (p) ::
ofLp : V
```
This reflects the syntax of the feature added in #7742 for overriding
binder kinds of structure projections. Similarly, only those parameters
in the header of the `structure` may be updated; it is an error to try
to update binder kinds of parameters included via `variable`.
Closes#9072.
Fixes a possible bug from stale caches when creating the type of the
constructor.
This PR adjusts the experimental module system to make `private` the
default visibility modifier in `module`s, introducing `public` as a new
modifier instead. `public section` can be used to revert the default for
an entire section, though this is more intended to ease gradual adoption
of the new semantics such as in `Init` (and soon `Std`) where they
should be replaced by a future decl-by-decl re-review of visibilities.
This PR allow structures to have non-bracketed binders, making it
consistent with `inductive`.
The change allows the following to be written instead of having to write
`S (n)`:
```lean
structure S n where
field : Fin n
```
This PR adds the pre-stage0-update infrastructure for named error
messages. It adds macro syntax for registering and throwing named errors
(without elaborators), mechanisms for displaying error names in the
Infoview and at the command line, and the ability to link to error
explanations in the manual (once they are added).
This PR adds the `#print sig $ident` variant of the `#print` command,
which omits the body. This is useful for testing meta-code, in the
```
#guard_msgs (drop trace, all) in #print sig foo
```
idiom. The benefit over `#check` is that it shows the declaration kind,
reducibility attributes (and in the future more built-in attributes,
like `@[defeq]` in #8419). (One downside is that `#check` shows unused
function parameter names, e.g. in induction principles; this could
probably be refined.)
This PR adjusts the experimental module system to not export the bodies
of `def`s unless opted out by the new attribute `@[expose]` on the `def`
or on a surrounding `section`.
---------
Co-authored-by: Markus Himmel <markus@lean-fro.org>
This PR modifies the `structure` syntax so that parents can be named,
like in
```lean
structure S extends toParent : P
```
**Breaking change:** The syntax is also modified so that the resultant
type comes *before* the `extends` clause, for example `structure S :
Prop extends P`. This is necessary to prevent a parsing ambiguity, but
also this is the natural place for the resultant type. Implements RFC
#7099.
Will need followup PRs for cleanup after a stage0 update.
This PR adds a `recommended_spelling` command, which can be used for
recording the recommended spelling of a notation (for example, that the
recommended spelling of `∧` in identifiers is `and`). This information
is then appended to the relevant docstrings for easy lookup.
The function `Lean.Elab.Term.Doc.allRecommendedSpellings` may be used to
obtain a list of all recommended spellings, for example to create a
table that is part of a style guide. In the future, it might be
desirable to be able to partition such a table into smaller tables by
category. This can be added in a future PR.
The implementation is heavily inspired by #4490.
This PR modifies structure instance notation and `where` notation to use
the same notation for fields. Structure instance notation now admits
binders, type ascriptions, and equations, and `where` notation admits
full structure lvals. Examples of these for structure instance notation:
```lean
structure PosFun where
f : Nat → Nat
pos : ∀ n, 0 < f n
def p : PosFun :=
{ f n := n + 1
pos := by simp }
def p' : PosFun :=
{ f | 0 => 1
| n + 1 => n + 1
pos := by rintro (_|_) <;> simp }
```
Just like for the structure `where` notation, a field `f x y z : ty :=
val` expands to `f := fun x y z => (val : ty)`. The type ascription is
optional.
The PR also is setting things up for future expansion. Pending some
discussion, in the future structure/`where` notation could have have
embedded `where` clauses; rather than `{ a := { x := 1, y := z } }` one
could write `{ a where x := 1; y := z }`.
As far as I can tell, the ability to pass a structure instance to a
deriving handler is not actually used in practice. It didn't seem to be
used in the test suite, at least.
Do we want to remove this, or do we want to use and document it? This PR
removes it, but that's not something I feel strongly about - but seeing
if it breaks Mathlib is a useful data point.
This command comes from Lean 3, which I had previously ported and
contributed to Batteries (née Std). In this new version, `#where`
produces actual command Syntax for all features of a top-level scope
(rather than splicing together strings), and it also now reports
included variables.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
This refactors and improves the `#eval` command, introducing some new
features.
* Now evaluated results can be represented using `ToExpr` and pretty
printing. This means **hoverable output**. If `ToExpr` fails, it then
tries `Repr` and then `ToString`. The `eval.pp` option controls whether
or not to try `ToExpr`.
* There is now **auto-derivation** of `Repr` instances, enabled with the
`pp.derive.repr` option (default to **true**). For example:
```lean
inductive Baz
| a | b
#eval Baz.a
-- Baz.a
```
It simply does `deriving instance Repr for Baz` when there's no way to
represent `Baz`. If core Lean gets `ToExpr` derive handlers, they could
be used here as well.
* The option `eval.type` controls whether or not to include the type in
the output. For now the default is false.
* Now things like `#eval do return 2` work. It tries using
`CommandElabM`, `TermElabM`, or `IO` when the monad is unknown.
* Now there is no longer `Lean.Eval` or `Lean.MetaEval`. These each used
to be responsible for both adapting monads and printing results. The
concerns have been split into two. (1) The `MonadEval` class is
responsible for adapting monads for evaluation (it is similar to
`MonadLift`, but instances are allowed to use default data when
initializing state) and (2) finding a way to represent results is
handled separately.
* Error messages about failed instance synthesis are now more precise.
Once it detects that a `MonadEval` class applies, then the error message
will be specific about missing `ToExpr`/`Repr`/`ToString` instances.
* Fixes a bug where `Repr`/`ToString` instances can't be found by
unfolding types "under the monad". For example, this works now:
```lean
def Foo := List Nat
def Foo.mk (l : List Nat) : Foo := l
#eval show Lean.CoreM Foo from do return Foo.mk [1,2,3]
```
* Elaboration errors now abort evaluation. This eliminates some
not-so-relevant error messages.
* Now evaluating a value of type `m Unit` never prints a blank message.
* Fixes bugs where evaluating `MetaM` and `CoreM` wouldn't collect log
messages.
The `run_cmd`, `run_elab`, and `run_meta` commands are now frontends for
`#eval`.
This solves the issue where certain subexpressions are lacking syntax
hovers because the hover text is not "builtin" - it only shows up if the
`Parser` constant is imported in the environment. For top level syntaxes
this is not a problem because `builtin_term_parser` will automatically
add this doc information, but nested syntaxes don't get the same
treatment.
We could walk the expression and add builtin docs recursively, but this
is somewhat expensive and unnecessary given that it's a fixed list of
declarations in lean core. Moreover, there are reasons to want to
control which syntax nodes actually get hovers, and while a better
system for that is forthcoming, for now it can be achieved by
strategically not applying the `@[builtin_doc]` attribute.
Fixes#3842
previously, `#eval` would happily evaluate expressions that contain
`sorry`, either explicitly or because of failing tactics. In conjunction
with operations like array access this can lead to the lean process
crashing, which isn't particularly great.
So how `#eval` will refuse to run code that (transitively) depends on
the `sorry` axiom (using the same code as `#print axioms`).
If the user really wants to run it, they can use `#eval!`.
Closes#1697
Also extends existing definition for `getScope`/`getScopes` and
clarifies that the `end` command is optional at the end of a file.
---------
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
