Leonardo de Moura 705530b62b fix: remove DecidableEq for Float ... We cannot implement `DecidableEq Float` using C equality for `double`. Reason: the C implementation is not even reflexive. If we need `DecidableEq Float`, we will need to provide our own implementation (i.e., a wrapper around the one provided by the hardware). In this commit, we implement `HasBeq Float` instead. cc @dselsam		2020-04-06 14:10:18 -07:00
..
Array	feat: generalize Array function universes	2020-04-06 13:48:09 -07:00
BinomialHeap	chore: Coe.lean ==> HasCoe.lean	2020-01-28 08:55:22 -08:00
ByteArray
Char	fix: support Windows newlines and '\r' escape	2020-03-27 13:21:21 -07:00
Fin	chore: HasModn ==> HasModN	2019-12-11 15:36:58 -08:00
HashMap	feat: add findEntry? functions	2020-02-24 15:47:59 -08:00
Int	refactor: String.toNat ==> String.toNat? and String.toNat!	2020-03-23 14:29:48 -07:00
List	feat: sort and deduplicate "expected" tokens in parser error messages	2020-03-19 17:17:08 -07:00
Nat	doc: expand dependent pattern matching support for array literals	2020-03-13 06:39:13 -07:00
Option	feat: add some useful helper functions I didn't actually use in the end	2020-03-19 17:14:31 -07:00
PersistentArray	refactor: naming consistency ensure List and Array have similar find* methods	2020-01-26 15:13:05 -08:00
PersistentHashMap	chore: variable order consistency	2020-02-24 18:29:24 -08:00
Queue
RBMap	chore: naming convention	2020-02-09 17:10:20 -08:00
RBTree	chore: naming convention	2020-02-09 17:10:20 -08:00
Stack
String	fix: missing file	2020-03-23 15:49:22 -07:00
Array.lean
AssocList.lean	feat: add findEntry? functions	2020-02-24 15:47:59 -08:00
Basic.lean	refactor: String.toNat ==> String.toNat? and String.toNat!	2020-03-23 14:29:48 -07:00
BinomialHeap.lean
ByteArray.lean
Char.lean
DList.lean	feat: add builtin notation	2019-12-11 16:22:23 -08:00
Fin.lean
Float.lean	fix: remove DecidableEq for Float	2020-04-06 14:10:18 -07:00
Hashable.lean	fix: leaks	2019-12-22 15:09:19 -08:00
HashMap.lean
HashSet.lean	perf: avoid unnecessary overhead at HashSet	2020-03-02 08:40:15 -08:00
Int.lean
List.lean
Nat.lean
Option.lean
PersistentArray.lean
PersistentHashMap.lean
PersistentHashSet.lean	feat: add findEntry? functions	2020-02-24 15:47:59 -08:00
Queue.lean
Random.lean	chore: avoid ^do ...	2019-12-11 06:19:12 -08:00
RBMap.lean
RBTree.lean
Repr.lean	feat: change ite and dite argument order	2020-02-03 14:11:29 -08:00
Stack.lean
String.lean	refactor: String.toNat ==> String.toNat? and String.toNat!	2020-03-23 14:29:48 -07:00
ToString.lean	feat: change ite and dite argument order	2020-02-03 14:11:29 -08:00
UInt.lean	feat: make sure Char.ofNat can be efficiently reduced in the kernel and WHNF	2020-03-18 16:41:48 -07:00