lean4-htt

Author	SHA1	Message	Date
Leonardo de Moura	ae5aa51712	chore: add explicit `discard`	2020-12-08 06:18:18 -08:00
Leonardo de Moura	0869f38de4	chore: update `structure`, `class`, `inductive`	2020-11-27 15:09:30 -08:00
Leonardo de Moura	898a08a0c1	chore: avoid `Has` prefix in type classes closes #203	2020-10-27 18:29:19 -07:00
Leonardo de Moura	13c2a8ff51	chore: remove `#lang lean4` header	2020-10-25 09:54:07 -07:00
Leonardo de Moura	0c89dca20e	chore: move to new frontend	2020-10-21 17:09:24 -07:00
Leonardo de Moura	0abca5475f	refactor: move `ppExpr` to `IO` @Kha I am also tracking `currNamespace` and `openDecls`. BTW, I also tried an experiment where I added `currNamespace` and `openDecls` to `Meta.Context`, but it looked weird. This information is only needed in the elaborator and pretty printer. The `PPContext` object should contain everything you need. You can put `currNamespace` and `openDecls` in the `Delaborator.Context`.	2020-09-15 18:48:21 -07:00
Sebastian Ullrich	7083aeea83	chore: adapt to upstream	2020-08-31 06:50:01 -07:00
Wojciech Nawrocki	bbcc718c8d	chore: more server fixes	2020-08-31 06:50:01 -07:00
Wojciech Nawrocki	7b9363c828	refactor: simplify document storage in server	2020-08-31 06:50:01 -07:00
Wojciech Nawrocki	633acebd0f	chore: server style fixes	2020-08-31 06:50:01 -07:00
Wojciech Nawrocki	7a7a14c8b9	chore: no leading commas	2020-08-31 06:50:01 -07:00
Wojciech Nawrocki	17acb78bb1	fix: more lenient server shutdown params	2020-08-31 06:50:01 -07:00
Wojciech Nawrocki	f3d640a7cf	feat: report parser errors in server	2020-08-31 06:50:01 -07:00
Wojciech Nawrocki	4356017035	chore: copyright	2020-08-31 06:50:01 -07:00
Wojciech Nawrocki	23feb04d60	chore: clean up LSP code style and add more definitions from the spec	2020-08-31 06:50:01 -07:00
Wojciech Nawrocki	098c7af1b6	feat: server tests	2020-08-31 06:50:01 -07:00

16 commits