max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
32271 commits 1 branch 0 tags 5.3 GiB
Commit graph

174 commits

Author SHA1 Message Date
Joe Hendrix
8b0dd2e835
chore: upstream Std.Logic (#3312) 
This will collect definitions from Std.Logic

---------

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
 2024-02-14 09:40:55 +00:00
Leonardo de Moura
c138801c3a
chore: rwa tactic macro (#3299) 2024-02-10 04:59:24 +00:00
Sebastian Ullrich
6b0e7e1f46
feat: synchronous execution of task continuations (#3013) 
In the new snapshot design, we have a tree of `Task`s that represents
the asynchronously processed document structure. When transforming this
tree in response to a user edit, we want to quickly run through
reusable, already computed nodes of the tree synchronously and then
spawn new tasks for the new parts. The new flag allows us to do such
mixed sync/async tree transformations uniformly. This flag exists as
e.g.
[`ExecuteSynchronously`](https://learn.microsoft.com/en-us/dotnet/api/system.threading.tasks.taskcontinuationoptions?view=net-8.0)
in other runtimes.
 2024-01-25 13:54:20 +00:00
Joe Hendrix
8293fd4e09
feat: cleanups to ACI and Identity classes (#3195) 
This makes changes to the definitions of Associativity, Commutativity,
Idempotence and Identity classes to be more aligned with Mathlib's
versions.

The changes are:
*  Move classes are moved from `Lean` to root namespace.
* Drop `Is` prefix from names.
* Rename `IsNeutral` to `LawfulIdentity` and add Left and Right
subclasses.
* Change neutral/identity element to outParam.
* Introduce `HasIdentity` for operations not intended for proofs to
implement

The identity changes are to make this compatible with
[Mathlib](718042db9d/Mathlib/Init/Algebra/Classes.lean)
and to enable nicer fold operations in Std that can use type classes to
infer the identity/initial element on binary operations.

---------

Co-authored-by: Kyle Miller <kmill31415@gmail.com>
 2024-01-24 21:46:58 +00:00
Scott Morrison
97f5ad7804
chore: change trustCompiler axiom to True (#2662) 2023-10-11 06:59:03 +00:00
Scott Morrison
833e778cd5
chore: add axiom for tracking use of reduceBool / reduceNat (#2654) 2023-10-11 01:47:59 +00:00
Siddharth
b9ec36d089
chore: get rid of all inline C annotations for LLVM (#2363) 2023-07-30 10:39:40 +02:00
Bulhwi Cha
3b6bc4a87d style: remove unnecessary space characters 2023-07-23 16:11:11 +02:00
Mario Carneiro
aa60791db3 feat: remove partial in Init.Data.String.Basic 2023-06-05 15:50:11 -07:00
Bulhwi Cha
445fd417be doc: add more explanations of quotients 
Add explanations of `Quotient.ind` and `Quotient.inductionOn` to
`Init.Core`.
 2023-05-05 12:22:59 -07:00
Bulhwi Cha
9fd1aeb0d8 fix: change the type of Quotient.ind 
Change the type of `Quotient.ind` by changing the type of `q` from
`Quot Setoid.r` to `Quotient s`.
 2023-05-05 12:22:59 -07:00
Gabriel Ebner
a2f5959118 chore: use deriving Nonempty 2022-12-22 03:48:15 +01:00
ChrisHughes24
e168806078 chore: rename Prod.ext 2022-12-02 20:24:19 +01:00
Leonardo de Moura
966e1df96d chore: fix build 2022-11-19 07:46:01 -08:00
Mario Carneiro
178d0ebe4f fix: protected on Nat.add_zero 2022-11-13 14:59:47 -08:00
Leonardo de Moura
95df68f3e4 chore: [elab_as_elim] at Eq.substr 
Lean 3 compatibility issue.

see #1806
 2022-11-07 19:44:11 -08:00
Leonardo de Moura
ad98df80fe feat: congr theorems using Iff 
closes #1763
 2022-10-26 18:00:24 -07:00
Mario Carneiro
583e023314 chore: snake-case attributes (part 2) 2022-10-19 09:28:08 -07:00
Mario Carneiro
dd5948d641 chore: snake-case attributes (part 1) 2022-10-19 09:28:08 -07:00
Gabriel Ebner
1c561c39a8 feat: function coercions with unification 2022-10-14 12:08:10 -07:00
Leonardo de Moura
e9d5dfc689 chore: closes #1683 2022-10-04 16:46:08 -07:00
Sebastian Ullrich
9e6814b09e doc: fix inline docs 2022-09-29 09:36:28 +02:00
Gabriel Ebner
f1b5fa53f0 chore: use new comment syntax 2022-09-14 08:26:17 -07:00
Gabriel Ebner
3bd0379993 chore: add nonempty instance for Task 2022-09-05 08:52:46 -07:00
Mario Carneiro
31784c9a24 doc: documentation for Init.Core 2022-08-29 00:41:24 -07:00
Mario Carneiro
5658000396 refactor: golf proof of funext 2022-08-28 19:01:46 -07:00
Mario Carneiro
f93914e613 fix: prove decidable_of_decidable_of_eq without cast 2022-08-28 08:32:00 -07:00
Mario Carneiro
d4c7d0f266 chore: remove def implies 2022-08-28 07:57:56 -07:00
Leonardo de Moura
50cecdbb62 chore: add Inhabited MProd and Inhabited PProd instances 
closes #1420
 2022-08-05 11:21:27 -07:00
Mario Carneiro
42a4f2f451 feat: ForIn instance for NameMap and PersistentHashMap 2022-07-31 15:42:26 -07:00
Leonardo de Moura
fbc6bcff92 chore: remove unnecessary french quotes 2022-07-29 20:53:01 -07:00
Leonardo de Moura
eafd2a88ce chore: simplify Prelude.lean and Core.lean using elabAsElim 2022-07-29 18:13:56 -07:00
Mario Carneiro
f6211b1a74
chore: convert doc/mod comments from /- to /--//-! (#1354) 2022-07-22 12:05:31 -07:00
Gabriel Ebner
c100f45b77 feat: add simp lemmas and instances for LawfulBEq 2022-07-11 14:19:41 -07:00
Leonardo de Moura
c9771fa1b2 chore: unused variables 2022-07-07 20:24:18 -07:00
François G. Dorais
bc206b2992 fix: LawfulBEq class 
make arguments implicit and protect `LawfulBEq.rfl`
 2022-06-16 15:33:32 -07:00
Leonardo de Moura
02c4e548df feat: replace constant with opaque 2022-06-14 17:02:59 -07:00
Leonardo de Moura
041827bed5 chore: unused variables 2022-06-07 17:54:10 -07:00
Leonardo de Moura
c2ddebc193 chore: unused variables 2022-06-07 16:47:04 -07:00
Sebastian Ullrich
897a5de6ac chore: revert some questionable signature changes 2022-06-07 16:37:45 -07:00
Sebastian Ullrich
fb2a2b3de2 fix: fixup previous commit 2022-06-07 16:37:45 -07:00
Sebastian Ullrich
ae7b895f7a refactor: unname some unused variables 2022-06-07 16:37:45 -07:00
Leonardo de Moura
2a36ae4627 feat: add List.le_antisymm 2022-04-20 16:31:25 -07:00
Leonardo de Moura
e00550c57e chore: remove {} occurrences 2022-04-13 10:14:51 -07:00
Daniel Fabian
cf4e873974 feat: support Sort u in ac_refl. 2022-03-16 17:21:20 -07:00
Daniel Fabian
1114dfac6c feat: add theory for ac normalization. 
This lets us implement an AC reflexivity tactic.
 2022-03-16 17:21:20 -07:00
Leonardo de Moura
99677823c3 fix: ForIn' instance binder annotations 2022-03-03 19:51:45 -08:00
Leonardo de Moura
d8ee03c1bb feat: add ForIn' instance that is similar to ForIn but provides a proof that the iterated elements are in the collection 2022-03-03 19:05:27 -08:00
Leonardo de Moura
89c3820781 chore: naming convention 2022-03-03 17:17:51 -08:00
Leonardo de Moura
eac5bab429 chore: helper theorem 2022-03-01 16:54:25 -08:00