-
Update
a[i]
notation. It is now based on the typeclassclass GetElem (Cont : Type u) (Idx : Type v) (Elem : outParam (Type w)) (Dom : outParam (Cont → Idx → Prop)) where getElem (xs : Cont) (i : Idx) (h : Dom xs i) : Elem
The notation
a[i]
is not defined as followsmacro:max x:term noWs "[" i:term "]" : term => `(getElem $x $i (by get_elem_tactic))
The proof that
i
is a valid index is synthesized using the tacticget_elem_tactic
. For example, the typeArray α
has the following instancesinstance : GetElem (Array α) Nat α fun xs i => LT.lt i xs.size where ... instance : GetElem (Array α) USize α fun xs i => LT.lt i.toNat xs.size where ...
You can use the notation
a[i]'h
to provide the proof manually. Two other notations were introduced:a[i]!
anda[i]?
, Fora[i]!
, a panic error message is produced at runtime ifi
is not a valid index.a[i]?
has typeOption α
, anda[i]?
evaluates tonone
if the indexi
is not valid. See discussion on Zulip. Examples:example (a : Array Int) (i : Nat) : Int := a[i] -- Error: failed to prove index is valid ... example (a : Array Int) (i : Nat) (h : i < a.size) : Int := a[i] -- Ok example (a : Array Int) (i : Nat) : Int := a[i]! -- Ok example (a : Array Int) (i : Nat) : Option Int := a[i]? -- Ok example (a : Array Int) (h : a.size = 2) : Int := a[0]'(by rw [h]; decide) -- Ok example (a : Array Int) (h : a.size = 2) : Int := have : 0 < a.size := by rw [h]; decide have : 1 < a.size := by rw [h]; decide a[0] + a[1] -- Ok example (a : Array Int) (i : USize) (h : i.toNat < a.size) : Int := a[i] -- Ok
-
Better support for qualified names in recursive declarations. The following is now supported:
namespace Nat def fact : Nat → Nat | 0 => 1 | n+1 => (n+1) * Nat.fact n end Nat
-
Update Lake to v3.2.1. See the v3.2.1 release notes for detailed changes.
-
Add support for
CommandElabM
monad at#eval
. Example:import Lean open Lean Elab Command #eval do let id := mkIdent `foo elabCommand (← `(def $id := 10)) #eval foo -- 10
-
Try to elaborate
do
notation even if the expected type is not available. We still delay elaboration when the expected type is not available. This change is particularly useful when writing examples such as#eval do IO.println "hello" IO.println "world"
That is, we don't have to use the idiom
#eval show IO _ from do ...
anymore. Note that auto monadic lifting is less effective when the expected type is not available. Monadic polymorphic functions (e.g.,ST.Ref.get
) also require the expected type. -
On Linux, panics now print a backtrace by default, which can be disabled by setting the environment variable
LEAN_BACKTRACE
to0
. Other platforms are TBD. -
The
group(·)
syntax
combinator is now introduced automatically where necessary, such as when using multiple parsers inside(...)+
. -
Add "Typed Macros": syntax trees produced and accepted by syntax antiquotations now remember their syntax kinds, preventing accidental production of ill-formed syntax trees and reducing the need for explicit
:kind
antiquotation annotations. See PR for details. -
Aliases of protected definitions are protected too. Example:
protected def Nat.double (x : Nat) := 2*x namespace Ex export Nat (double) -- Add alias Ex.double for Nat.double end Ex open Ex #check Ex.double -- Ok #check double -- Error, `Ex.double` is alias for `Nat.double` which is protected
-
Use
IO.getRandomBytes
to initialize random seed forIO.rand
. See discussion at this PR. -
Improve dot notation and aliases interaction. See discussion on Zulip for additional details. Example:
def Set (α : Type) := α → Prop def Set.union (s₁ s₂ : Set α) : Set α := fun a => s₁ a ∨ s₂ a def FinSet (n : Nat) := Fin n → Prop namespace FinSet export Set (union) -- FinSet.union is now an alias for `Set.union` end FinSet example (x y : FinSet 10) : FinSet 10 := x.union y -- Works
-
ext
andenter
conv tactics can now go inside let-declarations. Example:example (g : Nat → Nat) (y : Nat) (h : let x := y + 1; g (0+x) = x) : g (y + 1) = y + 1 := by conv at h => enter [x, 1, 1]; rw [Nat.zero_add] /- g : Nat → Nat y : Nat h : let x := y + 1; g x = x ⊢ g (y + 1) = y + 1 -/ exact h
-
Add
zeta
conv tactic to expand let-declarations. Example:example (h : let x := y + 1; 0 + x = y) : False := by conv at h => zeta; rw [Nat.zero_add] /- y : Nat h : y + 1 = y ⊢ False -/ simp_arith at h
-
Improve namespace resolution. See issue #1224. Example:
import Lean open Lean Parser Elab open Tactic -- now opens both `Lean.Parser.Tactic` and `Lean.Elab.Tactic`
-
Rename
constant
command toopaque
. See discussion at Zulip. -
Extend
induction
andcases
syntax: multiple left-hand-sides in a single alternative. This extension is very similar to the one implemented formatch
expressions. Examples:inductive Foo where | mk1 (x : Nat) | mk2 (x : Nat) | mk3 def f (v : Foo) := match v with | .mk1 x => x + 1 | .mk2 x => 2*x + 1 | .mk3 => 1 theorem f_gt_zero : f v > 0 := by cases v with | mk1 x | mk2 x => simp_arith! -- New feature used here! | mk3 => decide
-
Add unnamed antiquotation
$_
for use in syntax quotation patterns. -
Add unused variables linter. Feedback welcome!
-
Lean now generates an error if the body of a declaration body contains a universe parameter that does not occur in the declaration type, nor is an explicit parameter. Examples:
/- The following declaration now produces an error because `PUnit` is universe polymorphic, but the universe parameter does not occur in the function type `Nat → Nat` -/ def f (n : Nat) : Nat := let aux (_ : PUnit) : Nat := n + 1 aux ⟨⟩ /- The following declaration is accepted because the universe parameter was explicitly provided in the function signature. -/ def g.{u} (n : Nat) : Nat := let aux (_ : PUnit.{u}) : Nat := n + 1 aux ⟨⟩
-
Add
subst_vars
tactic. -
Fix
autoParam
in structure fields lost in multiple inheritance.. -
Add
[eliminator]
attribute. It allows users to specify default recursor/eliminators for theinduction
andcases
tactics. It is an alternative for theusing
notation. Example:@[eliminator] protected def recDiag {motive : Nat → Nat → Sort u} (zero_zero : motive 0 0) (succ_zero : (x : Nat) → motive x 0 → motive (x + 1) 0) (zero_succ : (y : Nat) → motive 0 y → motive 0 (y + 1)) (succ_succ : (x y : Nat) → motive x y → motive (x + 1) (y + 1)) (x y : Nat) : motive x y := let rec go : (x y : Nat) → motive x y | 0, 0 => zero_zero | x+1, 0 => succ_zero x (go x 0) | 0, y+1 => zero_succ y (go 0 y) | x+1, y+1 => succ_succ x y (go x y) go x y termination_by go x y => (x, y) def f (x y : Nat) := match x, y with | 0, 0 => 1 | x+1, 0 => f x 0 | 0, y+1 => f 0 y | x+1, y+1 => f x y termination_by f x y => (x, y) example (x y : Nat) : f x y > 0 := by induction x, y <;> simp [f, *]
-
Add support for
casesOn
applications to structural and well-founded recursion modules. This feature is useful when writing definitions using tactics. Example:inductive Foo where | a | b | c | pair: Foo × Foo → Foo def Foo.deq (a b : Foo) : Decidable (a = b) := by cases a <;> cases b any_goals apply isFalse Foo.noConfusion any_goals apply isTrue rfl case pair a b => let (a₁, a₂) := a let (b₁, b₂) := b exact match deq a₁ b₁, deq a₂ b₂ with | isTrue h₁, isTrue h₂ => isTrue (by rw [h₁,h₂]) | isFalse h₁, _ => isFalse (fun h => by cases h; cases (h₁ rfl)) | _, isFalse h₂ => isFalse (fun h => by cases h; cases (h₂ rfl))
-
Option
is again a monad. The auxiliary typeOptionM
has been removed. See Zulip thread. -
Improve
split
tactic. It used to fail onmatch
expressions of the formmatch h : e with ...
wheree
is not a free variable. The failure used to occur during generalization. -
New encoding for
match
-expressions that use theh :
notation for discriminants. The information is not lost during delaboration, and it is the foundation for a bettersplit
tactic. at delaboration time. Example:#print Nat.decEq /- protected def Nat.decEq : (n m : Nat) → Decidable (n = m) := fun n m => match h : Nat.beq n m with | true => isTrue (_ : n = m) | false => isFalse (_ : ¬n = m) -/
-
exists
tactic is now takes a comma separated list of terms. -
Add
dsimp
anddsimp!
tactics. They guarantee the result term is definitionally equal, and only applyrfl
-theorems. -
Fix binder information for
match
patterns that use definitions tagged with[matchPattern]
(e.g.,Nat.add
). We now have proper binder information for the variabley
in the following example.def f (x : Nat) : Nat := match x with | 0 => 1 | y + 1 => y
-
(Fix) the default value for structure fields may now depend on the structure parameters. Example:
structure Something (i: Nat) where n1: Nat := 1 n2: Nat := 1 + i def s : Something 10 := {} example : s.n2 = 11 := rfl
-
Apply
rfl
theorems at thedsimp
auxiliary method used bysimp
.dsimp
can be used anywhere in an expression because it preserves definitional equality. -
Refine auto bound implicit feature. It does not consider anymore unbound variables that have the same name of a declaration being defined. Example:
def f : f → Bool := -- Error at second `f` fun _ => true inductive Foo : List Foo → Type -- Error at second `Foo` | x : Foo []
Before this refinement, the declarations above would be accepted and the second
f
andFoo
would be treated as auto implicit variables. That is,f : {f : Sort u} → f → Bool
, andFoo : {Foo : Type u} → List Foo → Type
. -
Fix syntax hightlighting for recursive declarations. Example
inductive List (α : Type u) where | nil : List α -- `List` is not highlighted as a variable anymore | cons (head : α) (tail : List α) : List α def List.map (f : α → β) : List α → List β | [] => [] | a::as => f a :: map f as -- `map` is not highlighted as a variable anymore
-
Add
autoUnfold
option toLean.Meta.Simp.Config
, and the following macrossimp!
forsimp (config := { autoUnfold := true })
simp_arith!
forsimp (config := { autoUnfold := true, arith := true })
simp_all!
forsimp_all (config := { autoUnfold := true })
simp_all_arith!
forsimp_all (config := { autoUnfold := true, arith := true })
When the
autoUnfold
is set to true,simp
tries to unfold the following kinds of definition- Recursive definitions defined by structural recursion.
- Non-recursive definitions where the body is a
match
-expression. This kind of definition is only unfolded if thematch
can be reduced. Example:
def append (as bs : List α) : List α := match as with | [] => bs | a :: as => a :: append as bs theorem append_nil (as : List α) : append as [] = as := by induction as <;> simp_all! theorem append_assoc (as bs cs : List α) : append (append as bs) cs = append as (append bs cs) := by induction as <;> simp_all!
-
Add
save
tactic for creating checkpoints more conveniently. Example:example : <some-proposition> := by tac_1 tac_2 save tac_3 ...
is equivalent to
example : <some-proposition> := by checkpoint tac_1 tac_2 tac_3 ...
-
Remove support for
{}
annotation from inductive datatype contructors. This annotation was barely used, and we can control the binder information for parameter bindings using the new inductive family indices to parameter promotion. Example: the following declaration using{}
inductive LE' (n : Nat) : Nat → Prop where | refl {} : LE' n n -- Want `n` to be explicit | succ : LE' n m → LE' n (m+1)
can now be written as
inductive LE' : Nat → Nat → Prop where | refl (n : Nat) : LE' n n | succ : LE' n m → LE' n (m+1)
In both cases, the inductive family has one parameter and one index. Recall that the actual number of parameters can be retrieved using the command
#print
. -
Remove support for
{}
annotation in thestructure
command. -
Several improvements to LSP server. Examples: "jump to definition" in mutually recursive sections, fixed incorrect hover information in "match"-expression patterns, "jump to definition" for pattern variables, fixed auto-completion in function headers, etc.
-
In
macro ... xs:p* ...
and similar macro bindings of combinators,xs
now has the correct typeArray Syntax
-
Identifiers in syntax patterns now ignore macro scopes during matching.
-
Improve binder names for constructor auto implicit parameters. Example, given the inductive datatype
inductive Member : α → List α → Type u | head : Member a (a::as) | tail : Member a bs → Member a (b::bs)
before:
#check @Member.head -- @Member.head : {x : Type u_1} → {a : x} → {as : List x} → Member a (a :: as)
now:
#check @Member.head -- @Member.head : {α : Type u_1} → {a : α} → {as : List α} → Member a (a :: as)
-
Improve error message when constructor parameter universe level is too big.
-
Add support for
for h : i in [start:stop] do ..
whereh : i ∈ [start:stop]
. This feature is useful for proving termination of functions such as:inductive Expr where | app (f : String) (args : Array Expr) def Expr.size (e : Expr) : Nat := Id.run do match e with | app f args => let mut sz := 1 for h : i in [: args.size] do -- h.upper : i < args.size sz := sz + size (args.get ⟨i, h.upper⟩) return sz
-
Add tactic
case'
. It is similar tocase
, but does not admit the goal on failure. For example, the new tactic is useful when writing tactic scripts where we need to usecase'
atfirst | ... | ...
, and we want to take the next alternative whencase'
fails. -
Add tactic macro
macro "stop" s:tacticSeq : tactic => `(repeat sorry)
See discussion on Zulip.
-
When displaying goals, we do not display inaccessible proposition names if they do not have forward dependencies. We still display their types. For example, the goal
case node.inl.node β : Type u_1 b : BinTree β k : Nat v : β left : Tree β key : Nat value : β right : Tree β ihl : BST left → Tree.find? (Tree.insert left k v) k = some v ihr : BST right → Tree.find? (Tree.insert right k v) k = some v h✝ : k < key a✝³ : BST left a✝² : ForallTree (fun k v => k < key) left a✝¹ : BST right a✝ : ForallTree (fun k v => key < k) right ⊢ BST left
is now displayed as
case node.inl.node β : Type u_1 b : BinTree β k : Nat v : β left : Tree β key : Nat value : β right : Tree β ihl : BST left → Tree.find? (Tree.insert left k v) k = some v ihr : BST right → Tree.find? (Tree.insert right k v) k = some v : k < key : BST left : ForallTree (fun k v => k < key) left : BST right : ForallTree (fun k v => key < k) right ⊢ BST left
-
The hypothesis name is now optional in the
by_cases
tactic. -
Fix inconsistency between
syntax
and kind names. The node kindsnumLit
,charLit
,nameLit
,strLit
, andscientificLit
are now callednum
,char
,name
,str
, andscientific
respectively. Example: we now writemacro_rules | `($n:num) => `("hello")
instead of
macro_rules | `($n:numLit) => `("hello")
-
(Experimental) New
checkpoint <tactic-seq>
tactic for big interactive proofs. -
Rename tactic
nativeDecide
=>native_decide
. -
Antiquotations are now accepted in any syntax. The
incQuotDepth
syntax
parser is therefore obsolete and has been removed. -
Renamed tactic
nativeDecide
=>native_decide
. -
"Cleanup" local context before elaborating a
match
alternative right-hand-side. Examples:example (x : Nat) : Nat := match g x with | (a, b) => _ -- Local context does not contain the auxiliary `_discr := g x` anymore example (x : Nat × Nat) (h : x.1 > 0) : f x > 0 := by match x with | (a, b) => _ -- Local context does not contain the `h✝ : x.fst > 0` anymore
-
Improve
let
-pattern (andhave
-pattern) macro expansion. In the following example,example (x : Nat × Nat) : f x > 0 := by let (a, b) := x done
The resulting goal is now
... |- f (a, b) > 0
instead of... |- f x > 0
. -
Add cross-compiled aarch64 Linux and aarch64 macOS releases.
-
Add tutorial-like examples to our documentation, rendered using LeanInk+Alectryon.
-
simp
now takes user-defined simp-attributes. You can define a newsimp
attribute by creating a file (e.g.,MySimp.lean
) containingimport Lean open Lean.Meta initialize my_ext : SimpExtension ← registerSimpAttr `my_simp "my own simp attribute"
If you don't neet to acces
my_ext
, you can also use the macroimport Lean register_simp_attr my_simp "my own simp attribute"
Recall that the new
simp
attribute is not active in the Lean file where it was defined. Here is a small example using the new feature.import MySimp def f (x : Nat) := x + 2 def g (x : Nat) := x + 1 @[my_simp] theorem f_eq : f x = x + 2 := rfl @[my_simp] theorem g_eq : g x = x + 1 := rfl example : f x + g x = 2*x + 3 := by simp_arith [my_simp]
-
Extend
match
syntax: multiple left-hand-sides in a single alternative. Example:def fib : Nat → Nat | 0 | 1 => 1 | n+2 => fib n + fib (n+1)
This feature was discussed at issue 371. It was implemented as a macro expansion. Thus, the following is accepted.
inductive StrOrNum where | S (s : String) | I (i : Int) def StrOrNum.asString (x : StrOrNum) := match x with | I a | S a => toString a
-
Improve
#eval
command. Now, when it fails to synthesize aLean.MetaEval
instance for the result type, it reduces the type and tries again. The following example now works without additional annotationsdef Foo := List Nat def test (x : Nat) : Foo := [x, x+1, x+2] #eval test 4
-
rw
tactic can now apply auto-generated equation theorems for a given definition. Example:example (a : Nat) (h : n = 1) : [a].length = n := by rw [List.length] trace_state -- .. |- [].length + 1 = n rw [List.length] trace_state -- .. |- 0 + 1 = n rw [h]
-
Extend dot-notation
x.field
for arrow types. If type ofx
is an arrow, we look up forFunction.field
. For example, givenf : Nat → Nat
andg : Nat → Nat
,f.comp g
is now notation forFunction.comp f g
. -
The new
.<identifier>
notation is now also accepted where a function type is expected.example (xs : List Nat) : List Nat := .map .succ xs example (xs : List α) : Std.RBTree α ord := xs.foldl .insert ∅
-
Support notation
let <pattern> := <expr> | <else-case>
indo
blocks. -
Remove support for "auto"
pure
. In the Zulip thread, the consensus seemed to be that "auto"pure
is more confusing than it's worth. -
Remove restriction in
congr
theorems that all function arguments on the left-hand-side must be free variables. For example, the following theorem is now a validcongr
theorem.@[congr] theorem dep_congr [DecidableEq ι] {p : ι → Set α} [∀ i, Inhabited (p i)] : ∀ {i j} (h : i = j) (x : p i) (y : α) (hx : x = y), Pi.single (f := (p ·)) i x = Pi.single (f := (p ·)) j ⟨y, hx ▸ h ▸ x.2⟩ :=
-
Improve elaboration postponement heuristic when expected type is a metavariable. Lean now reduces the expected type before performing the test.
-
Remove deprecated leanpkg in favor of Lake now bundled with Lean.
-
Various improvements to go-to-definition & find-all-references accuracy.
-
Auto generated congruence lemmas with support for casts on proofs and
Decidable
instances (see whishlist). -
Rename option
autoBoundImplicitLocal
=>autoImplicit
. -
Relax auto-implicit restrictions. The command
set_option relaxedAutoImplicit false
disables the relaxations. -
contradiction
tactic now closes the goal if there is aFalse.elim
application in the target. -
Renamed tatic
byCases
=>by_cases
(motivation: enforcing naming convention). -
Local instances occurring in patterns are now considered by the type class resolution procedure. Example:
def concat : List ((α : Type) × ToString α × α) → String | [] => "" | ⟨_, _, a⟩ :: as => toString a ++ concat as
-
Notation for providing the motive for
match
expressions has changed. before:match x, rfl : (y : Nat) → x = y → Nat with | 0, h => ... | x+1, h => ...
now:
match (motive := (y : Nat) → x = y → Nat) x, rfl with | 0, h => ... | x+1, h => ...
With this change, the notation for giving names to equality proofs in
match
-expressions is not whitespace sensitive anymore. That is, we can now writematch h : sort.swap a b with | (r₁, r₂) => ... -- `h : sort.swap a b = (r₁, r₂)`
-
(generalizing := true)
is the default behavior formatch
expressions even if the expected type is not a proposition. In the following example, we used to have to include(generalizing := true)
manually.inductive Fam : Type → Type 1 where | any : Fam α | nat : Nat → Fam Nat example (a : α) (x : Fam α) : α := match x with | Fam.any => a | Fam.nat n => n
-
We now use
PSum
(instead ofSum
) when compiling mutually recursive definitions using well-founded recursion. -
Better support for parametric well-founded relations. See issue #1017. This change affects the low-level
termination_by'
hint because the fixed prefix of the function parameters in not "packed" anymore when constructing the well-founded relation type. For example, in the following definition,as
is part of the fixed prefix, and is not packed anymore. In previous versions, thetermination_by'
term would be written asmeasure fun ⟨as, i, _⟩ => as.size - i
def sum (as : Array Nat) (i : Nat) (s : Nat) : Nat := if h : i < as.size then sum as (i+1) (s + as.get ⟨i, h⟩) else s termination_by' measure fun ⟨i, _⟩ => as.size - i
-
Add
while <cond> do <do-block>
,repeat <do-block>
, andrepeat <do-block> until <cond>
macros fordo
-block. These macros are based onpartial
definitions, and consequently are useful only for writing programs we don't want to prove anything about. -
Add
arith
option toSimp.Config
, the macrosimp_arith
expands tosimp (config := { arith := true })
. OnlyNat
and linear arithmetic is currently supported. Example:example : 0 < 1 + x ∧ x + y + 2 ≥ y + 1 := by simp_arith
-
Add
fail <string>?
tactic that always fail. -
Add support for acyclicity at dependent elimination. See issue #1022.
-
Add
trace <string>
tactic for debugging purposes. -
Add nontrivial
SizeOf
instance for typesUnit → α
, and add support for them in the auto-generatedSizeOf
instances for user-defined inductive types. For example, given the inductive datatypeinductive LazyList (α : Type u) where | nil : LazyList α | cons (hd : α) (tl : LazyList α) : LazyList α | delayed (t : Thunk (LazyList α)) : LazyList α
we now have
sizeOf (LazyList.delayed t) = 1 + sizeOf t
instead ofsizeOf (LazyList.delayed t) = 2
. -
Add support for guessing (very) simple well-founded relations when proving termination. For example, the following function does not require a
termination_by
annotation anymore.def Array.insertAtAux (i : Nat) (as : Array α) (j : Nat) : Array α := if h : i < j then let as := as.swap! (j-1) j; insertAtAux i as (j-1) else as
-
Add support for
for h : x in xs do ...
notation whereh : x ∈ xs
. This is mainly useful for showing termination. -
Auto implicit behavior changed for inductive families. An auto implicit argument occurring in inductive family index is also treated as an index (IF it is not fixed, see next item). For example
inductive HasType : Index n → Vector Ty n → Ty → Type where
is now interpreted as
inductive HasType : {n : Nat} → Index n → Vector Ty n → Ty → Type where
-
To make the previous feature more convenient to use, we promote a fixed prefix of inductive family indices to parameters. For example, the following declaration is now accepted by Lean
inductive Lst : Type u → Type u | nil : Lst α | cons : α → Lst α → Lst α
and
α
inLst α
is a parameter. The actual number of parameters can be inspected using the command#print Lst
. This feature also makes sure we still accept the declarationinductive Sublist : List α → List α → Prop | slnil : Sublist [] [] | cons l₁ l₂ a : Sublist l₁ l₂ → Sublist l₁ (a :: l₂) | cons2 l₁ l₂ a : Sublist l₁ l₂ → Sublist (a :: l₁) (a :: l₂)
-
Added auto implicit "chaining". Unassigned metavariables occurring in the auto implicit types now become new auto implicit locals. Consider the following example:
inductive HasType : Fin n → Vector Ty n → Ty → Type where | stop : HasType 0 (ty :: ctx) ty | pop : HasType k ctx ty → HasType k.succ (u :: ctx) ty
ctx
is an auto implicit local in the two constructors, and it has typectx : Vector Ty ?m
. Without auto implicit "chaining", the metavariable?m
will remain unassigned. The new feature creates yet another implicit localn : Nat
and assignsn
to?m
. So, the declaration above is shorthand forinductive HasType : {n : Nat} → Fin n → Vector Ty n → Ty → Type where | stop : {ty : Ty} → {n : Nat} → {ctx : Vector Ty n} → HasType 0 (ty :: ctx) ty | pop : {n : Nat} → {k : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType k ctx ty → HasType k.succ (u :: ctx) ty
-
Eliminate auxiliary type annotations (e.g,
autoParam
andoptParam
) from recursor minor premises and projection declarations. Consider the following examplestructure A := x : Nat h : x = 1 := by trivial example (a : A) : a.x = 1 := by have aux := a.h -- `aux` has now type `a.x = 1` instead of `autoParam (a.x = 1) auto✝` exact aux example (a : A) : a.x = 1 := by cases a with | mk x h => -- `h` has now type `x = 1` instead of `autoParam (x = 1) auto✝` assumption
-
We now accept overloaded notation in patterns, but we require the set of pattern variables in each alternative to be the same. Example:
inductive Vector (α : Type u) : Nat → Type u | nil : Vector α 0 | cons : α → Vector α n → Vector α (n+1) infix:67 " :: " => Vector.cons -- Overloading the `::` notation def head1 (x : List α) (h : x ≠ []) : α := match x with | a :: as => a -- `::` is `List.cons` here def head2 (x : Vector α (n+1)) : α := match x with | a :: as => a -- `::` is `Vector.cons` here
-
New notation
.<identifier>
based on Swift. The namespace is inferred from the expected type. See issue #944. Examples:def f (x : Nat) : Except String Nat := if x > 0 then .ok x else .error "x is zero" namespace Lean.Elab open Lsp def identOf : Info → Option (RefIdent × Bool) | .ofTermInfo ti => match ti.expr with | .const n .. => some (.const n, ti.isBinder) | .fvar id .. => some (.fvar id, ti.isBinder) | _ => none | .ofFieldInfo fi => some (.const fi.projName, false) | _ => none def isImplicit (bi : BinderInfo) : Bool := bi matches .implicit end Lean.Elab