Leonardo de Moura 6dddcde25c chore: increase priority of defaultInstance for heterogeneous operators ... @Kha The motivation is to allow users to define default instances such as ```lean @[defaultInstance 1] instance : OfScientific Real where ... ``` Then, numerals such as `1.2` and `3.4e10` will be `Real` by default instead of `Float`.		2020-12-07 16:58:34 -08:00
..
Control	fix: <&>	2020-12-01 11:57:20 -08:00
Data	refactor: OfDecimal ==> OfScientific	2020-12-03 08:08:19 -08:00
System	fix: bug at runST and runEST	2020-12-06 18:52:28 -08:00
Classical.lean	chore: use exists notation	2020-12-05 16:50:01 -08:00
Coe.lean	feat: heterogeneous OrElse and AndThen	2020-12-01 18:32:24 -08:00
Control.lean	chore: merge src/Control files	2020-11-10 18:47:23 -08:00
Core.lean	chore: adjust stdlib	2020-11-29 17:01:56 -08:00
Data.lean	refactor: OfDecimal ==> OfScientific	2020-12-03 08:08:19 -08:00
Fix.lean	refactor: arbitrary without explicit arguments	2020-11-25 09:07:38 -08:00
Meta.lean	refactor: OfDecimal ==> OfScientific	2020-12-03 08:08:19 -08:00
Notation.lean	fix: make "$" ws atomic so it doesn't eat up later antiquotations	2020-12-04 19:24:32 +01:00
NotationExtra.lean	feat: scoped and local unification hints	2020-12-05 14:34:14 -08:00
Prelude.lean	chore: increase priority of defaultInstance for heterogeneous operators	2020-12-07 16:58:34 -08:00
SizeOf.lean	chore: update structure, class, inductive	2020-11-27 15:09:30 -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: update structure, class, inductive	2020-11-27 15:09:30 -08:00