Wojciech Nawrocki
a4cb8249d9
chore: fixup after rebase
2020-08-31 06:50:01 -07:00
Marc Huisinga
1b3d254dd0
feat: add emptyEnv and add initSearchPath temporarily so that server binary finds LEAN_PATH
2020-08-31 06:50:01 -07:00
Wojciech Nawrocki
86582ac73c
feat: edits seem to work now
2020-08-31 06:50:01 -07:00
Wojciech Nawrocki
46803ca25b
feat: working diagnostics (modulo line numbers)
2020-08-31 06:50:01 -07:00
Marc Huisinga
e7b3d0be59
feat: initial server implementation
2020-08-31 06:50:01 -07:00
Leonardo de Moura
1103806ff4
refactor: HasMonadLift ==> MonadLift
2020-08-25 13:54:41 -07:00
Leonardo de Moura
b672f0820b
chore: remove workarounds
2020-08-23 19:56:01 -07:00
Leonardo de Moura
77b9445544
feat: real ST monad
...
@Kha: the new `ST` (and `EST`) are escapable like the Haskell ST monad.
It makes `StateRefT` much more useful because we can now run it from pure
code.
2020-08-23 12:15:32 -07:00
Leonardo de Moura
5ffbada3df
feat: add Lean.MonadEnv, Lean.MonadError, and Lean.MonadOptions
...
This is the first set of polymorphic methods. I will add more later,
and keep reducing code duplication.
cc @Kha
2020-08-22 16:00:43 -07:00
Leonardo de Moura
d36ccb166c
feat: use EIO Empty instead of IO at IO.Ref primitives
2020-08-20 12:54:15 -07:00
Sebastian Ullrich
0e8ef0cb8c
chore: document Format fields
2020-08-06 09:26:48 -07:00
Leonardo de Moura
6e279be7af
chore: add Name.getString!
2020-07-20 15:18:45 -07:00
Leonardo de Moura
cbb14673ef
chore: move RBTree and RBMap to Std
2020-06-25 13:26:16 -07:00
Leonardo de Moura
1612097788
chore: move HashMap and HashSet to Std
2020-06-25 12:46:56 -07:00
Leonardo de Moura
1be221a1f4
chore: move PersistentHashMap and PersistentHashSet to Std
2020-06-25 11:56:00 -07:00
Leonardo de Moura
2dd1d3ac3e
chore: move ShareCommon to Std
2020-06-25 11:45:29 -07:00
Leonardo de Moura
249bda16c0
chore: remove prelude commands from Lean package
2020-06-25 11:21:17 -07:00
Sebastian Ullrich
6614b4d6e3
fix: use exact instead of prefix token match when inheriting precedence
...
/cc @leodemoura :)
2020-05-28 14:14:52 +02:00
Leonardo de Moura
4ccc3fef52
chore: move Init.Lean files to Lean package
2020-05-26 15:04:35 -07:00
