Leonardo de Moura
68fc9a9115
feat: add dummy mpz implementation for LEAN_USE_GMP=OFF
2021-11-29 11:42:08 -08:00
Leonardo de Moura
0002d8bd04
chore: missing #ifdef LEAN_USE_GMP
2021-11-29 11:35:13 -08:00
Leonardo de Moura
6396f3b2c1
chore: simplify mpz.h
...
Add basic support for `LEAN_USE_GMP=OFF`.
2021-11-29 11:11:49 -08:00
Leonardo de Moura
7435fd5dd4
chore: add USE_GMP cmake option
2021-11-29 10:25:26 -08:00
Sebastian Ullrich
0764967757
fix: getFVarId
2021-11-29 10:06:15 -08:00
Sebastian Ullrich
465913c391
fix: this must be a keyword
2021-11-29 10:06:15 -08:00
Sebastian Ullrich
531eefb7db
chore: adapt syntax
2021-11-29 10:06:15 -08:00
Sebastian Ullrich
9cca1a57e0
feat: generalize syntax of fvar-accepting tactics
2021-11-29 10:06:15 -08:00
Joshua Seaton
a9317760e7
chore: update IR interpreter enum hygiene
...
This change addresses -Wreturn type and -Wimplicit-fallthrough
infractions in the IR interpreter. Moreover, default switch cases on
enum classes are removed to leverage compiler complaints of missing
cases, which ensures that all related switch logic gets thoughtfully
extended when the enums are extended themselves.
2021-11-28 10:29:08 +01:00
Sebastian Ullrich
a329896e70
feat: refine declaration ranges at instance & example
2021-11-27 07:25:15 -08:00
Sebastian Ullrich
4f15805787
feat: annotate declarations with term infos
2021-11-27 07:25:15 -08:00
Leonardo de Moura
0aa32d643e
fix: eta struct and proof irrelevance issue
...
see #777
2021-11-27 07:15:57 -08:00
Leonardo de Moura
2d113e83f9
feat: eta struct support for unit-like datatypes
...
For example, given `a b : Unit`, we have that `a` and `b` are
definitionally equal by `etaStruct`.
See #777
2021-11-26 08:36:25 -08:00
Leonardo de Moura
f9a5ac1d8e
fix: missing condition at matchConstStruct
2021-11-26 08:36:25 -08:00
Leonardo de Moura
693a96681a
doc: fix eta struct comment
2021-11-26 08:36:25 -08:00
Sebastian Ullrich
676b5e5ea8
chore: typo
...
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
2021-11-26 17:13:19 +01:00
Sebastian Ullrich
14bc140efe
fix: server: do not show parent node on synthetic sorry
2021-11-26 17:13:19 +01:00
Sebastian Ullrich
4063729b6c
doc: document some built-in term notations
2021-11-26 17:13:19 +01:00
Sebastian Ullrich
2a1aee2b7a
feat: record declaration ranges of builtin parsers & elaborators
2021-11-26 17:13:19 +01:00
Sebastian Ullrich
e9f7c88299
feat: record doc strings of builtin parsers & elaborators
2021-11-26 17:13:19 +01:00
Sebastian Ullrich
8176084dcf
refactor: factor out declareBuiltin
2021-11-26 17:13:19 +01:00
larsk21
e641ae4eae
fix: prefix check in set_option completion
2021-11-26 11:42:54 +01:00
Leonardo de Moura
3ccd44fafa
fix: proofs after adding eta struct support at recursors
...
see #777
2021-11-25 11:34:31 -08:00
Leonardo de Moura
88b6ad4756
feat: add etaStruct to Meta.Simp.Config
2021-11-25 11:31:00 -08:00
Leonardo de Moura
d806344ee2
fix: set etaStruct := false at MatchEqns
2021-11-25 11:31:00 -08:00
Leonardo de Moura
43217884c0
feat: add Meta.Config.etaStruct
...
It is useful to disable eta for structures for meta programs.
2021-11-25 11:31:00 -08:00
Leonardo de Moura
0fc8c1da77
feat: eta for structures at recursors
...
see #777
2021-11-25 11:31:00 -08:00
Leonardo de Moura
50ac21d0a6
refactor: move is_constructor_app to inductive.cpp
2021-11-25 11:31:00 -08:00
Leonardo de Moura
e22bffa94f
refactor: move is_structure_like to inductive.cpp
2021-11-25 11:31:00 -08:00
Leonardo de Moura
03e346bc66
chore: simplify to_cnstr_when_K
2021-11-25 11:31:00 -08:00
Leonardo de Moura
9e1704f658
chore: simplify toCtorWhenK
2021-11-25 11:31:00 -08:00
Leonardo de Moura
ccc3f99507
chore: use isStructureLike
2021-11-25 11:31:00 -08:00
Leonardo de Moura
0de700fe45
chore: naming convetion
2021-11-25 11:31:00 -08:00
Sebastian Ullrich
f7decd2d46
fix: go to definition for macro_rules etc.
2021-11-24 11:54:13 +01:00
Wojciech Nawrocki
17f99e353e
fix: tactic state at EOF
2021-11-24 09:15:56 +01:00
Leonardo de Moura
a8f4146070
feat: support eta struct recursively
...
Addresses issues raised by @gebner at #777
2021-11-23 17:38:48 -08:00
Sebastian Ullrich
653ff184a8
fix: semantic highlighting, once more
2021-11-23 17:20:01 +01:00
Sebastian Ullrich
573c3c9760
fix: semantic highlighting, again
2021-11-23 17:02:09 +01:00
Gabriel Ebner
7537fa7795
fix: unfold x<y in discrimination tree module
2021-11-23 07:34:51 -08:00
Leonardo de Moura
e15a656fd2
fix: remove @[reducible] annotation from Function.comp and Function.const
...
closes #813
2021-11-23 07:29:25 -08:00
Leonardo de Moura
9fde1d53b7
chore: adjust proofs affected by struct eta
...
closes #777
2021-11-23 06:23:50 -08:00
Leonardo de Moura
d685c545b4
feat: eta for structures
2021-11-23 06:21:25 -08:00
Sebastian Ullrich
dd146d50cf
fix: extra linker flags (e.g. -ldl) must come after stdlib linker flags
2021-11-23 13:07:05 +01:00
Sebastian Ullrich
12306ba401
fix: -lgmp should come last
2021-11-23 13:07:05 +01:00
Sebastian Ullrich
226121433f
fix: semantic highlighting of projection notation elaborated twice
2021-11-23 13:01:51 +01:00
Varun Gandhi
9ae6380b43
fix: only check for ccache if variables aren't passed explicitly
...
The existing CMake will emit a spurious warning when someone
tries to explicitly pass CMAKE_C(XX)_COMPILER_LAUNCHER, such
as when they point it to sccache instead of ccache.
2021-11-23 09:15:42 +01:00
Scott Morrison
43315f7f94
fix: correct spacing in the pretty printer
2021-11-23 09:13:31 +01:00
Leonardo de Moura
d9b057af03
fix: fixes #793
2021-11-22 13:28:08 -08:00
Gabriel Ebner
f55649f81b
fix: prefer simp lemmas with *higher* priority
2021-11-22 11:52:45 -08:00
larsk21
9028405798
fix: handle _root_ in unresolveNameGlobal with pp.fullNames
2021-11-21 15:23:21 +01:00
