Commit graph

4 commits

Author SHA1 Message Date
Leonardo de Moura
a76b104f61 chore: move Message to Lean 2020-01-10 10:58:50 -08:00
Leonardo de Moura
cc5a3cca29 chore: move helper modules to src/Init/Lean/Util 2019-12-04 17:17:34 -08:00
Leonardo de Moura
f15af1df0a chore: move Lean auxiliary datatypes to src/Init/Lean/Data 2019-12-04 17:00:13 -08:00
Leonardo de Moura
c445199747 chore: library/Init ==> src/Init
cc @Kha @dselsam @cipher1024
2019-11-22 06:06:05 -08:00
Renamed from library/Init/Lean/Message.lean (Browse further)