Daniel Fabian ed75005422 feat: make proofs Hashable ... change the `Hashable` class from taking a hash function of `Type u` to taking a hash function from `Sort u`. This allows to implement `Hashable` for propositions, which in turn is needed for inductives carrying proofs		2021-03-30 13:36:52 -07:00
..
Control	chore: remove when and «unless»	2021-03-20 18:52:18 -07:00
Data	feat: make proofs Hashable	2021-03-30 13:36:52 -07:00
System	chore: remove leftovers	2021-03-23 17:33:23 -07:00
Classical.lean	refactor: cases	2021-03-07 12:37:02 -08:00
Coe.lean	feat: CoeSort Bool Prop	2021-03-20 14:52:16 +01:00
Control.lean	feat: add ExceptCpsT	2021-02-27 18:44:24 -08:00
Core.lean	chore: use "discriminant refinement"	2021-03-24 10:43:43 -07:00
Data.lean	feat: add helper classes for implementing parallel for	2020-12-19 14:15:47 -08:00
Fix.lean	refactor: arbitrary without explicit arguments	2020-11-25 09:07:38 -08:00
Hints.lean	fix: Not should not be reducible, special support for Ne	2021-02-15 17:36:11 -08:00
Meta.lean	chore: remove dead code	2021-03-29 20:37:49 -07:00
Notation.lean	feat: add trivial extensible (macro) tactic	2021-03-24 09:50:56 -07:00
NotationExtra.lean	feat: basic unexpanders for Exists & Sigma	2021-02-04 11:04:37 +01:00
Prelude.lean	feat: make proofs Hashable	2021-03-30 13:36:52 -07:00
SimpLemmas.lean	feat: add missing simp lemmas for ->	2021-03-24 14:51:18 -07:00
SizeOf.lean	chore: define SizeOf Lean.Name instance manually	2021-01-20 18:07:14 -08:00
System.lean	chore: remove #lang lean4 header	2020-10-25 09:54:07 -07:00
Util.lean	feat: add Prelude.lean	2020-11-10 18:08:18 -08:00
WF.lean	chore: remove unnecessary generalizing	2021-03-27 15:03:13 -07:00