Leonardo de Moura
f26c905130
refactor: split Structural.lean into smaller files
2021-09-11 03:40:51 -07:00
Leonardo de Moura
964095ba6e
chore: clean up before refactoring
2021-09-11 02:58:55 -07:00
Sebastian Ullrich
eb1e285e26
chore: style
2021-06-21 10:17:26 -07:00
Daniel Fabian
9200de01ef
refactor: fix code review comments.
2021-06-06 06:40:09 -07:00
Daniel Fabian
968ae18f20
fix: deal with params for inductive predicates.
2021-06-06 06:40:09 -07:00
Daniel Fabian
4e53b3bdbf
fix: use motive from brecOn in structural recursion for predicates.
2021-06-06 06:40:09 -07:00
Daniel Fabian
822c551aa2
test: Add a bunch of test for structural recursion on predicates.
2021-06-06 06:40:09 -07:00
Daniel Fabian
ec6f7d9bd6
feat: Implement structural recursion for inductive predicates.
2021-06-06 06:40:09 -07:00
Leonardo de Moura
96b5574f21
fix: use withoutProofIrrelevance at getFixedPrefix
2021-05-27 13:42:22 -07:00
Leonardo de Moura
1a2a089c28
chore: comment
2021-04-13 10:34:19 -07:00
Leonardo de Moura
adda3a9e02
fix: improve structural recursion
2021-04-13 10:31:43 -07:00
Leonardo de Moura
59d7008f24
chore: cleanup
2021-04-13 08:12:14 -07:00
Leonardo de Moura
be841a7cad
chore: throwError! => throwError, throwErrorAt! => throwErrorAt
...
@Kha I marked the corresponding methods as `protected`.
I currently can't stand `throw_error`, and I am optimistic about
server highlighting feature you are working on :)
2021-03-11 11:59:45 -08:00
Leonardo de Moura
68143ca8ba
chore: trace[...]! ==> trace[...]
...
@Kha I think this one is a good change, there is no real reason for
using the `!` suffix here.
2021-03-10 18:44:43 -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
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
f0ac477d2e
feat: add sanity checks
2021-01-01 18:31:28 -08:00
Leonardo de Moura
04a07c15b9
chore: use deriving Inhabited
2020-12-13 11:57:59 -08:00
Leonardo de Moura
0869f38de4
chore: update structure, class, inductive
2020-11-27 15:09:30 -08:00
Leonardo de Moura
c9cbe35916
fix: adjust code to optional , at structure instances
...
@Kha I implemented the optional `,` at structure instances.
You have suggested it a few weeks/months ago. F# also implements this
feature. I got back to it while write documentation for Lean.
It looks quite nice when we are packing many functions into a structure.
BTW, F# also has optional separators for list literals :)
This is a much simpler change for us since `[...]` is defined using
the `syntax/macro_rules` commands, but I didn't find optional ','
would very useful since our list literals are usually in a single
line.
2020-11-20 15:43:35 -08:00
Leonardo de Moura
f67c93191f
feat: use |>.
2020-11-19 08:38:47 -08:00
Leonardo de Moura
57670b633a
feat: improve smart unfolding
2020-11-16 15:44:52 -08:00
Leonardo de Moura
461c0786fd
feat: generate auxiliary declaration for "smart unfolding"
2020-11-15 16:31:40 -08:00
Leonardo de Moura
98cc4639a0
fix: nested recursive applications
2020-11-14 18:01:22 -08:00
Leonardo de Moura
db5fe843de
chore: add expandInterpolatedStr helper function, rename msg! => m!
2020-11-14 13:52:52 -08:00
Leonardo de Moura
82d6dd2eb6
feat: improve Structural.lean
2020-11-09 13:23:25 -08:00
Leonardo de Moura
2d2d39c78e
chore: use mut
2020-11-07 17:32:13 -08:00
Leonardo de Moura
1e30d0831d
feat: allow recursive application in the discriminant of a nested match
2020-11-07 17:32:12 -08:00
Leonardo de Moura
81d6e065e7
chore: adjust files and tests
2020-11-07 17:32:12 -08:00
Leonardo de Moura
13c2a8ff51
chore: remove #lang lean4 header
2020-10-25 09:54:07 -07:00
Leonardo de Moura
3f0cc1d2ec
fix: library/constructions primitives crash at kernel_exception
2020-10-24 18:52:01 -07:00
Leonardo de Moura
e8c1647fa5
chore: improve condition
2020-10-24 12:37:11 -07:00
Leonardo de Moura
84926f62ea
chore: improve error message
2020-10-24 08:16:05 -07:00
Leonardo de Moura
01251a56e0
chore: improve error message
2020-10-24 07:57:02 -07:00
Leonardo de Moura
0af4b6fb6f
chore: remove hack that produces big search space
2020-10-24 07:21:06 -07:00
Leonardo de Moura
525fb7ca91
chore: cleanup
2020-10-24 06:26:32 -07:00
Leonardo de Moura
1495f403a1
chore: use builtin_initialize instead of initialize at src/Lean
2020-10-19 15:17:02 -07:00
Leonardo de Moura
45e1300414
fix: nested structural recursion
2020-10-18 10:38:51 -07:00
Leonardo de Moura
b1e720e6cc
chore: use #lang lean4 instead of new_frontend
2020-10-15 15:40:56 -07:00
Leonardo de Moura
bdb92ce7a4
feat: add throwError! macro and improve trace[..]! macro
2020-10-13 12:32:33 -07:00
Leonardo de Moura
0c626f3e5d
chore: move to new frontend
...
chore: cleanup
2020-10-13 12:00:20 -07:00
Leonardo de Moura
d0bcb43c33
feat: improve Structural.lean
2020-10-12 16:58:30 -07:00
Leonardo de Moura
a3218dd063
refactor: export Core.mkFreshUserName to Lean namespace
2020-09-30 11:21:46 -07:00
Leonardo de Moura
240680db1a
feat: add binductionOn support
2020-09-25 07:18:14 -07:00
Leonardo de Moura
1775d9b04b
fix: visit types
...
See new test `tests/lean/run/def14.lean`
2020-09-25 06:48:51 -07:00
Leonardo de Moura
0e16bd60dc
fix: missing case
2020-09-25 06:48:51 -07:00
Leonardo de Moura
e4f492d68a
feat: add support for reflexive inductive datatypes
2020-09-24 20:30:12 -07:00
Leonardo de Moura
98f7e9b3e4
chore: naming convention
2020-09-24 19:22:24 -07:00
Leonardo de Moura
53acb2b56f
chore: naming convention
2020-09-24 17:50:17 -07:00
