max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add example to RELEASES.md

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-03 11:28:37 -08:00
parent 02d7cedba8
commit 30409fc73d
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
RELEASES.md
View file

@ -83,7 +83,11 @@ termination_by' measure fun ⟨i, _⟩ => as.size - i
* Add `while <cond> do <do-block>`, `repeat <do-block>`, and `repeat <do-block> until <cond>` macros for `do`-block. These macros are based on `partial` definitions, and consequently are useful only for writing programs we don't want to prove anything about.
* Add `arith` option to `Simp.Config`, the macro `simp_arith` expands to `simp (config := { arith := true })`. Only `Nat` and linear arithmetic is currently supported.
* Add `arith` option to `Simp.Config`, the macro `simp_arith` expands to `simp (config := { arith := true })`. Only `Nat` and linear arithmetic is currently supported. Example:
```lean
example : 0 < 1 + x ∧ x + y + 2 ≥ y + 1 := by
simp_arith
```
* Add `fail <string>?` tactic that always fail.
@ -101,7 +105,7 @@ inductive LazyList (α : Type u) where
we now have `sizeOf (LazyList.delayed t) = 1 + sizeOf t` instead of `sizeOf (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.
```
```lean
def Array.insertAtAux (i : Nat) (as : Array α) (j : Nat) : Array α :=
if h : i < j then
let as := as.swap! (j-1) j;