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
b5afc34391
chore: update stage0
2021-11-26 08:38:34 -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
093fd48e48
chore: update stage0
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
cec573024c
chore: update stage0
2021-11-25 11:32:53 -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
8f88b1f3f8
feat: bundle llvm-ar with Lean
2021-11-25 15:05:06 +01:00
Sebastian Ullrich
9a939f98ec
chore: update stage0
2021-11-24 15:04:27 +01: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
292d3218c2
chore: update stage0
2021-11-23 17:40:44 -08: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
Leonardo de Moura
c447db5db9
chore: update stage0
2021-11-23 07:36:16 -08: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
8af1024931
chore: update stage0
2021-11-23 06:23:06 -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
ammkrn
80c04c562a
doc: add/edit macro guide
...
Incorporate review changes to the doc book suggested by Kha.
2021-11-22 11:02:07 +01:00
ammkrn
7539799976
doc: add macro guide, light reorganizing
...
Sebastian suggested moving the macro guide from Mathlib4 upstream into the Lean 4 manual (called `macro_overview.md` here). There was some discussion about where to put it; the section on metaprogramming seemed like the most appropriate place. I did a little bit of reorganizing to make some items more discoverable (e.g. the user-defined notation section).
2021-11-22 11:02:07 +01:00
larsk21
9028405798
fix: handle _root_ in unresolveNameGlobal with pp.fullNames
2021-11-21 15:23:21 +01:00
