Leonardo de Moura
d4f7899591
chore: avoid code duplication setting Simp.Config
2022-01-24 18:57:31 -08:00
Leonardo de Moura
dae3489fe2
feat: remove partials from Init/Data/Array/Basic.lean
2022-01-10 16:05:33 -08:00
Leonardo de Moura
7789779020
feat: add simple default tactic for well-founded recursion
2022-01-10 14:26:08 -08:00
tydeu
f4a73889e7
feat: expose more version info (e..g., toolchain)
2021-12-19 10:44:35 +01:00
Sebastian Ullrich
167dccce0b
chore: move Leanpkg.leanVersionString to Init
2021-12-18 10:59:37 -08:00
Sebastian Ullrich
a4633d30e2
fix: option completion after trailing .
2021-12-10 14:19:19 -08:00
Leonardo de Moura
68bd55af32
chore: fix codebase
2021-12-10 13:12:09 -08:00
Leonardo de Moura
88b6ad4756
feat: add etaStruct to Meta.Simp.Config
2021-11-25 11:31:00 -08:00
Sebastian Ullrich
b5e7b2ab6e
feat: Lean.githash
2021-11-04 15:29:48 -07:00
Gabriel Ebner
bfc74decde
feat: add info field to Syntax.node
2021-10-26 20:19:27 +02:00
Leonardo de Moura
fc1ec438b8
fix: Repr Name instance
2021-09-18 15:29:32 -07:00
Leonardo de Moura
2a9ba9f795
fix: add support for hierachical names containing numerical parts
...
closes #677
2021-09-17 19:21:49 -07:00
Leonardo de Moura
d2240a99e5
feat: add erw tactic back as a macro
2021-09-12 19:29:12 -07:00
Leonardo de Moura
ea37c64b52
feat: add Meta.Rewrite.Config
2021-09-12 18:44:08 -07:00
Wojciech Nawrocki
77365abc8b
chore: Repr Syntax and minor cleanup
2021-08-24 08:57:41 -07:00
Leonardo de Moura
a821dcbff2
chore: enforce naming convention for theorems
...
see issue #402
fix: `ElabTerm.lean`
2021-08-07 12:48:38 -07:00
Sebastian Ullrich
8637220927
fix: make precedence mandatory for mixfix commands
...
Resolves #577
2021-07-19 13:18:58 -07:00
Wojciech Nawrocki
f07e49acdb
chore: parse names properly
2021-07-19 09:55:37 +02:00
Sebastian Ullrich
99e2a57791
chore: remove unused field Simp.Config.ctorEq
...
Resolves #553
2021-07-05 09:02:20 +02:00
Sebastian Ullrich
a02c6fd3eb
chore: adapt stdlib & tests
2021-05-20 15:17:36 -07:00
Sebastian Ullrich
23f0c1051c
feat: improve ToString/Quote Name
2021-05-19 09:34:01 +02:00
Leonardo de Moura
3b7bcdc449
feat: add endPos field to SourceInfo.original
...
We need an update stage0 before we use it.
2021-05-17 14:32:58 -07:00
Leonardo de Moura
ac90052139
feat: add option for controlling how deep we go when trying to discharge simp theorem hypotheses
2021-05-16 12:32:05 -07:00
Leonardo de Moura
7398db5f3f
fix: rw final goal state
2021-05-04 16:58:44 -07:00
Leonardo de Moura
6efb058e2c
refactor: add Name.modifyBase
2021-05-03 10:06:20 -07:00
Sebastian Ullrich
e76fc17b0e
fix: rw goal state positions
2021-05-03 14:14:12 +02:00
Leonardo de Moura
7de9cfeac8
chore: fix StructInst and add mkGroupNode
2021-04-07 22:46:07 -07:00
Leonardo de Moura
ca314f1aa4
refactor: add helper functions for match syntax elaborator
2021-04-06 19:02:03 -07:00
Leonardo de Moura
3db5b7e4ca
chore: remove dead code
2021-03-29 20:37:49 -07:00
Leonardo de Moura
f75d9f50a6
feat: (try to) improve InfoTree.goalsAt?
2021-03-29 18:43:33 -07:00
Leonardo de Moura
564d0fe1cd
chore: add getHeadPos?
2021-03-29 16:55:29 -07:00
Leonardo de Moura
ec5afce45b
feat: contextual := true at simp_all
...
cc @Kha
2021-03-24 15:49:31 -07:00
Leonardo de Moura
04e3f21783
chore: add OptionM monad
...
Motivation: `Option` is data, `OptionM` is control.
2021-03-20 17:50:45 -07:00
Leonardo de Moura
bf8119a5cd
chore: convert keywords to snake_case
...
Again `!` is only for functions that can panic.
2021-03-12 13:34:51 -08:00
Leonardo de Moura
5662e2e745
refactor: move ToString Syntax and BEq Syntax to Init
2021-02-26 13:21:04 -08:00
Leonardo de Moura
1c5de9842d
feat: use decide at simp
2021-02-15 13:08:45 -08:00
Leonardo de Moura
d834d88b88
fix: performance bottleneck
...
@Kha @dselsam
The instances
```
instance (sep) : Coe (Array Syntax) (SepArray sep)
instance (sep) : Coe (SepArray sep) (Array Syntax)
```
The instances above generate a loop. The current `isNewAnswer`
predicate is too weak and assumes that answers with different
metavariables are different. Note that, using `isDefEq` there is
incorrect and too expensive. I will fix this later in the future.
In the meantime, I am using `CoeTail` to avoid the loop.
2021-01-24 17:45:50 -08:00
Sebastian Ullrich
21a826ee51
chore: naming
2021-01-20 22:47:18 +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
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
4752c56fe8
feat: improve range of missing cases: ... error message
...
@Kha I added the helper combinator `withHeadRefOnly x`. I executes `x`
using the head token of the current `ref` as the new `ref`.
2021-01-14 14:48:53 -08:00
Leonardo de Moura
791388400b
feat: improve do error messages
...
cc @Kha @Vtec234
2021-01-14 14:18:56 -08:00
Leonardo de Moura
bfc1a16c02
chore: adjust instance param order
2021-01-13 18:31:41 -08:00
Leonardo de Moura
e742dd1348
feat: allow user to set Simp.Config at simp
2021-01-01 15:12:18 -08:00
Sebastian Ullrich
6e33020da4
feat: version information API
2020-12-29 14:42:48 -08:00
Leonardo de Moura
ccefe970dc
feat: store endPos at Log.lean
2020-12-23 19:09:41 -08:00
Sebastian Ullrich
cf73233dd2
refactor: use quotations & implicit token positions from getRef to clean up a bit
2020-12-21 17:32:36 +01:00
Leonardo de Moura
bbcd2247f2
feat: extend valid set of valid auto bound names
...
@Kha The motivation was Andrew's example :)
Users often use `u₁`, `u1`, `u₂`, ... to name universe variables.
2020-12-19 12:36:19 -08:00
