Gabriel Ebner
|
7356840cbc
|
feat: use sepBy1Indent for tactic blocks
|
2022-09-18 16:43:23 -07:00 |
|
Leonardo de Moura
|
b6f0bdc542
|
chore: add Array.mapMono
|
2022-08-30 11:45:05 -07:00 |
|
Leonardo de Moura
|
4f5a014170
|
feat: add Array.mapMonoM
|
2022-08-28 08:55:35 -07:00 |
|
Leonardo de Moura
|
e9bcc779fe
|
feat: add Array.mapM'
|
2022-08-03 11:18:19 -07:00 |
|
Mario Carneiro
|
25aea1b723
|
doc: document all the tactics
|
2022-08-01 08:08:03 -07:00 |
|
Mario Carneiro
|
f6211b1a74
|
chore: convert doc/mod comments from /- to /--//-! (#1354)
|
2022-07-22 12:05:31 -07:00 |
|
Leonardo de Moura
|
2fcd406f99
|
chore: remove sorry
|
2022-07-10 20:04:06 -07:00 |
|
Leonardo de Moura
|
475c7e18cd
|
chore: missing GetElem instances
|
2022-07-10 14:53:22 -07:00 |
|
Leonardo de Moura
|
2f1b80721e
|
chore: avoid a[i]' h notation
|
2022-07-10 07:20:07 -07:00 |
|
Leonardo de Moura
|
aa52eebcdc
|
feat: add instance GetElem (Array α) USize α fun xs i => LT.lt i.toNat xs.size where
|
2022-07-09 16:18:29 -07:00 |
|
Leonardo de Moura
|
1caff852fb
|
chore: remove getOp functions
|
2022-07-09 16:09:28 -07:00 |
|
Leonardo de Moura
|
e4b358a01e
|
refactor: prepare to elaborate a[i] notation using typeclasses
|
2022-07-09 15:24:22 -07:00 |
|
Leonardo de Moura
|
5e3a3a6c21
|
chore: remove notation a[i,h] for a[⟨i, h⟩]
|
2022-07-03 06:24:26 -07:00 |
|
Leonardo de Moura
|
54c60d4c2d
|
feat: a[i] and a[i]! notation for Subarrays
|
2022-07-02 15:54:34 -07:00 |
|
Leonardo de Moura
|
a2456c3a0f
|
feat: add notation a[i, h] for a[⟨i, h⟩]
|
2022-07-02 15:50:49 -07:00 |
|
Leonardo de Moura
|
3f3cd22366
|
feat: add Array.getOp! and Array.getOp?
Add warning when `Array.getOp` is used. TODO: replace `Array.getOp`
with safe version
|
2022-07-02 10:06:05 -07:00 |
|
E.W.Ayers
|
a7c33a963f
|
doc: docstrings for List.isPrefixOf
|
2022-06-17 17:47:51 -07:00 |
|
Leonardo de Moura
|
f6d1e48cb8
|
fix: constant => opaque issues
|
2022-06-14 17:19:54 -07:00 |
|
Wojciech Nawrocki
|
ff15e31e85
|
refactor: remove redundant theorem
|
2022-06-12 14:01:05 -07:00 |
|
Leonardo de Moura
|
041827bed5
|
chore: unused variables
|
2022-06-07 17:54:10 -07:00 |
|
Sebastian Ullrich
|
ae7b895f7a
|
refactor: unname some unused variables
|
2022-06-07 16:37:45 -07:00 |
|
Leonardo de Moura
|
34bbe5d12c
|
feat: add simp theorem List.of_toArray_eq_toArray (as bs : List α) : (as.toArray = bs.toArray) = (as = bs) := by
|
2022-05-27 18:26:48 -07:00 |
|
François G. Dorais
|
155b41937a
|
fix: remove unnecessary hypothesis (#1144)
|
2022-05-07 15:39:37 -07:00 |
|
Leonardo de Moura
|
24417ed466
|
feat: size, get, get!, getD, and getOp for Subarray
|
2022-04-29 09:55:45 -07:00 |
|
Leonardo de Moura
|
de2e2447d2
|
chore: style
|
2022-04-07 17:35:05 -07:00 |
|
Leonardo de Moura
|
64cfbc1ae3
|
feat: add helper tactic for applying sizeOf (a.get i) < sizeOf a automatically in termination proofs
|
2022-04-02 18:29:41 -07:00 |
|
Leonardo de Moura
|
03ec8cb30b
|
feat: missing sizeOf theorems for Array.get and List.get
|
2022-04-02 16:04:46 -07:00 |
|
Leonardo de Moura
|
cfb4e306f7
|
refactor: replace length_dropLast theorem
|
2022-04-01 16:44:24 -07:00 |
|
zygi
|
ac793ce196
|
fix: forward start and stop in Array.allM
|
2022-03-17 10:08:40 +01:00 |
|
Sebastian Ullrich
|
82c682d385
|
chore: remove redundant proof
|
2022-03-12 11:12:56 +01:00 |
|
Leonardo de Moura
|
5caf1bc692
|
chore: style
Use `·` instead of `.` for structuring tactics.
|
2022-03-11 16:12:46 -08:00 |
|
Leonardo de Moura
|
e1424653b9
|
chore: remove workaround
|
2022-03-03 18:16:54 -08:00 |
|
Leonardo de Moura
|
aeb9b2fb8c
|
chore: add Membership instance for Array
|
2022-03-03 18:13:34 -08:00 |
|
Leonardo de Moura
|
5845002e8c
|
feat: use WF at anyM
|
2022-03-03 16:43:05 -08:00 |
|
Leonardo de Moura
|
02d7cedba8
|
chore: remove unnecessary termination_by annotations
|
2022-03-03 11:24:06 -08:00 |
|
Leonardo de Moura
|
19bcb5fb31
|
feat: add Array.popWhile and Array.takeWhile
|
2022-02-19 07:04:52 -08:00 |
|
Leonardo de Moura
|
bd89bdde8a
|
fix: core library
see #1018
|
2022-02-15 12:12:56 -08:00 |
|
Sebastian Ullrich
|
54522006f4
|
refactor: List.get: take Fin to align with Array.get
/cc @leodemoura
|
2022-02-15 18:41:22 +01:00 |
|
Leonardo de Moura
|
9cfa728eac
|
chore: remove workaround for issue #1013
|
2022-02-11 09:32:29 -08:00 |
|
Leonardo de Moura
|
77bbaf82df
|
feat: decidable equality for arrays
|
2022-02-10 17:31:03 -08:00 |
|
Leonardo de Moura
|
1d5da63482
|
chore: simplify Array.isEqvAux
|
2022-02-10 16:51:47 -08:00 |
|
Leonardo de Moura
|
12e2a79170
|
chore: fix codebase after removing auto pure
|
2022-02-03 18:08:14 -08:00 |
|
Gabriel Ebner
|
561a869e49
|
fix: provide reference implementation for Array.modify
|
2022-01-17 12:41:12 -08:00 |
|
Leonardo de Moura
|
bac91b9b5b
|
chore: remove arbitrary
|
2022-01-15 12:14:27 -08:00 |
|
Leonardo de Moura
|
acd482c5f2
|
feat: define Array.modify without using Inhabited
|
2022-01-14 19:47:42 -08:00 |
|
Leonardo de Moura
|
7fe6881c42
|
feat: use new termination_by syntax
|
2022-01-12 16:23:25 -08:00 |
|
Leonardo de Moura
|
381f66428a
|
chore: use termination_by'
We are going to define a higher level syntax for `termination_by`.
|
2022-01-11 15:00:53 -08:00 |
|
Leonardo de Moura
|
93f3773d83
|
chore: cleanup
|
2022-01-10 16:25:07 -08:00 |
|
Leonardo de Moura
|
dae3489fe2
|
feat: remove partials from Init/Data/Array/Basic.lean
|
2022-01-10 16:05:33 -08:00 |
|
Leonardo de Moura
|
68bd55af32
|
chore: fix codebase
|
2021-12-10 13:12:09 -08:00 |
|