Wojciech Nawrocki
8addea6e74
chore: remove Handle.size
2021-01-22 18:02:31 +01:00
Sebastian Ullrich
0c91b3769e
chore: replace variables in src/
2021-01-22 14:36:05 +01:00
Sebastian Ullrich
8a02dfec4f
feat: subsume variables under variable
...
/cc @leodemoura
2021-01-22 14:36:05 +01:00
Leonardo de Moura
d6eb5a9ff2
feat: generate sizeOf equality lemmas for constructors
...
TODO: support for nested inductive types.
2021-01-21 17:44:15 -08:00
Leonardo de Moura
1f88d66035
feat: add missing instances
2021-01-21 10:35:22 -08:00
Sebastian Ullrich
941a68165a
fix: hover/definition for applications with only implicit arguments
2021-01-21 17:23:17 +01:00
Sebastian Ullrich
c1a07e5687
chore: Nix: delete obsolete workaround
2021-01-21 15:01:40 +01:00
Sebastian Ullrich
2a45525b24
chore: clean up code
2021-01-21 15:00:38 +01:00
Sebastian Ullrich
fbb1184f25
feat: auto-add stdlib to LEAN_SRC_PATH for installed Lean
2021-01-21 14:18:52 +01:00
Leonardo de Moura
e8401ea6e7
chore: remove old instances
2021-01-20 18:12:35 -08:00
Leonardo de Moura
7c6d09496e
chore: define SizeOf Lean.Name instance manually
2021-01-20 18:07:14 -08:00
Leonardo de Moura
46c62a3fed
chore: add missing instances
2021-01-20 17:53:43 -08:00
Leonardo de Moura
2b6e3bb696
chore: do not generate SizeOf instance for classes
2021-01-20 17:48:27 -08:00
Leonardo de Moura
ce11b23a59
feat: use deriving insertion sizeOf for types defined at Prelude.lean
2021-01-20 17:48:17 -08:00
Leonardo de Moura
65ffb15dff
feat: add mkSizeOfHandler
2021-01-20 17:18:51 -08:00
Leonardo de Moura
4ffc2c93cd
feat: invoke mkSizeOfInstances from structure and inductive commands
2021-01-20 17:07:02 -08:00
Leonardo de Moura
80e547ae98
feat: add mkSizeOfInstances
2021-01-20 17:07:02 -08:00
Leonardo de Moura
ad913de340
refactor: define SizeOf before Core.lean
2021-01-20 17:07:02 -08:00
Leonardo de Moura
4615ae743a
feat: add mkSizeOfFns
2021-01-20 17:07:02 -08:00
Leonardo de Moura
ea0fda39bc
chore: Declaration.lean naming convention
...
`Declaration.lean` was one of the first Lean 4 files, and was still
using an old naming convention.
cc @Kha
2021-01-20 17:07:02 -08:00
Leonardo de Moura
d428c388cf
feat: generater minor premises for sizeOf function rec application
2021-01-20 17:07:01 -08:00
Leonardo de Moura
eaace14d55
feat: add helper functions for creating +, *, - applications
2021-01-20 17:07:01 -08:00
Leonardo de Moura
6c63780a81
chore: use double quote
...
This commit also fixes a typo at `Option.cons`
2021-01-20 17:07:01 -08:00
Sebastian Ullrich
771f023cd3
fix: preserve syntheticness in resolveName'
2021-01-20 22:47:18 +01:00
Sebastian Ullrich
b94c5c181c
chore: annotate syntheticness in info format
2021-01-20 22:47:18 +01:00
Sebastian Ullrich
21a826ee51
chore: naming
2021-01-20 22:47:18 +01:00
Mohamed Al-Fahim
53750ddae6
chore: fix typos
2021-01-20 22:43:25 +01:00
Leonardo de Moura
21812541ea
fix: solve method at isLevelDefEq
...
closes #283
2021-01-20 08:36:26 -08:00
Leonardo de Moura
6a89a811ce
chore: cleanup
2021-01-20 08:36:26 -08:00
Leonardo de Moura
901a89a58c
chore: cleanup
2021-01-20 08:36:26 -08:00
Sebastian Ullrich
316b453be4
chore: do not show term info for synthetic sorry
2021-01-20 16:48:50 +01:00
Sebastian Ullrich
67c78ef1b7
fix: exclude synthetic syntax from hover/definition
2021-01-20 16:48:50 +01:00
Sebastian Ullrich
a9f96ace3e
chore: naming
2021-01-20 16:48:50 +01:00
Sebastian Ullrich
79107a2316
feat: copy & store whole ref range in SourceInfo
2021-01-20 16:48:50 +01:00
Sebastian Ullrich
1e623a961f
chore: debug assertion
2021-01-20 16:48:50 +01:00
Sebastian Ullrich
5f392749f2
chore: remove dead code
2021-01-20 16:48:50 +01:00
Sebastian Ullrich
462e1d54a3
chore: replace uses of copyInfo with automatic position copying in syntax quotations
...
We could introduce a `copyPos` alternative, but turns out we don't need it right now
2021-01-20 16:48:50 +01:00
Sebastian Ullrich
51e408590f
chore: do not copy whitespace in Syntax synth helpers
2021-01-20 16:48:50 +01:00
Leonardo de Moura
e57a9fa78f
fix: fixes #280
...
We are going to use a cleaner fix when we port this code to Lean.
2021-01-19 18:01:52 -08:00
Leonardo de Moura
8c6a510e65
fix: use withReducible
...
`def17.lean` contains example where `isDefEq arg x` takes a very long
time with the default reducibility test.
2021-01-19 18:01:52 -08:00
Leonardo de Moura
c1bc0e44f6
fix: fixes #281
...
This issue exposed two bugs at `Structural.lean`
1- `getFixedPrefix` was using structural equality to detected fixed
arguments. We should use definitional equality.
2- The `replaceFVars` was broken. We should use `instantiateForall` instead.
2021-01-19 18:01:52 -08:00
Leonardo de Moura
1e7380a1f7
fix: fixes #282
2021-01-19 18:01:52 -08:00
Leonardo de Moura
8e39b82541
feat: skeleton for SizeOf instance generator
2021-01-19 18:01:52 -08:00
Wojciech Nawrocki
445420315e
fix: normalise go-to-def paths
2021-01-19 13:22:13 -08:00
Wojciech Nawrocki
90075153b3
fix: UTF-16 strikes again
...
We need to report the jump target range in terms of a UTF-16 offset within the line, but to compute that we would have to load the target file, file-map it, and resolve that way each time the go-to-def handler runs. As an alternative, this stores the UTF-16 offsets in `DeclarationRange`.
2021-01-19 13:22:13 -08:00
Wojciech Nawrocki
e627ad308d
feat: go-to-definition
2021-01-19 13:22:13 -08:00
Wojciech Nawrocki
40698ecc07
feat: LSP scaffolding for go-to-definition
2021-01-19 13:22:13 -08:00
Wojciech Nawrocki
f07cf2c4e4
feat: store source path in server worker
2021-01-19 13:22:13 -08:00
Wojciech Nawrocki
f252a47bbb
feat: generalise SearchPath lookup
2021-01-19 13:22:13 -08:00
Sebastian Ullrich
bc0f43c4b9
chore: remove a few dbgTraceVals...
2021-01-19 19:31:44 +01:00
