Chris Lovett
ad7c5b26a7
fix: UTF-8 file path support for lean on Windows
...
* fix msys2 windows build so the windows apps support utf-8 file paths.
* use windres to compile default-manifest.o
* windres is in binutils.
* stop modifying default-manifest.o
* copy to stage0
* fix semicolon joining of lists in add_custom_target
* undo changes to stage0 as per CR feedback.
* fix makefile
* fix: revert cmakelists.txt COMMAND_EXPAND_LISTS change
* fix: msys2 dependencies
* add unit test for decoding UTF-8 chars to prove "lean.exe" can read utf-8 encoded files where utf-8 is also used in the file name.
* fix: utf-8 test by using windows-2022
* fix: do we really need cmake 3.11 or will 3.10 do?
* nope, really does require cmake 11.
2021-09-22 12:21:52 +02:00
Leonardo de Moura
6b1bed5c38
chore: fix test output
2021-09-21 20:37:23 -07:00
Leonardo de Moura
a909e8cf26
feat: arity mismatch error message at well-founded recursion
2021-09-21 20:34:15 -07:00
Leonardo de Moura
6a880fecc9
chore: modify findDocString?
2021-09-21 17:29:40 -07:00
Leonardo de Moura
640fc964b6
feat: basic termination_by bookkeeping
2021-09-21 15:24:42 -07:00
Leonardo de Moura
d43876ac2d
chore: fix test
2021-09-21 14:54:45 -07:00
Leonardo de Moura
9085167872
test: Fin match test that relies heavily on contradiction
...
This example is based on a Lean 3 issue described at
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/equation.20compiler.20help.20me.20plz
2021-09-21 12:57:08 -07:00
Leonardo de Moura
0351c96831
feat: better error message for induction tactic on mutually inductives
2021-09-21 06:56:17 -07:00
Sebastian Ullrich
15109b5f23
chore: remove obsolete file
2021-09-21 15:54:16 +02:00
Leonardo de Moura
2cbf0ba8e9
test: add "parameters" that are fixed in all equations
2021-09-20 12:58:22 -07:00
Leonardo de Moura
41a58459d7
test: equational theorem generation
2021-09-20 11:12:42 -07:00
Leonardo de Moura
9e980b2a78
fix: bug at decAux?
...
We are getting a few "stuck at universe constraint" errors after the
fix. We may need to add some kind of approximation in the future.
2021-09-20 07:12:57 -07:00
Leonardo de Moura
f2a418a7ae
chore: smartUnfolding cleanup
...
We remove dead code, update comments, and add new tests
See #445
2021-09-19 15:29:11 -07:00
Leonardo de Moura
fe55205105
test: equational theorem test
2021-09-19 09:34:08 -07:00
Leonardo de Moura
82f3042fa4
fix: equational theorem generation for structural recursion
2021-09-19 08:48:40 -07:00
Leonardo de Moura
c2d33a1a58
fix: bug at addSmartUnfoldingDef
...
The approach using `matcherBelowDep : NameSet` was not correct because
we "reuse" matcher-declarations. For example, in the definition
```
def f : Nat → Bool
| 0 => true
| n + 1 => (match n with
| 0 => true
| _ + 1 => true) && f n
```
we have to `match`-expressions but they can be compiled the same
matcher `f.match_1`. Thus, the set `matcherBelowDep` would contain
`f.match_1` since the first occurence refined the `Nat.below` argument
at `mkBRecOn`. Thus, `addSmartUnfoldingDef` was incorrectly assuming the second
`match` was refined too.
We fixed this issue by simulating `mkBRecOn` behavior.
fixes #445
2021-09-18 19:15:38 -07:00
Leonardo de Moura
c795a75045
feat: modify approach for generating equational theorems
2021-09-18 15:58:31 -07:00
Leonardo de Moura
fe7b750bce
fix: fixes #679
2021-09-18 15:34:29 -07: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
d413aa1dc5
feat: generate proofs for structural (conditional) equality theorems
2021-09-17 18:57:39 -07:00
Leonardo de Moura
1a0badac06
feat: generate conditional structural equation theorem types
...
TODO: proofs
2021-09-17 16:49:30 -07:00
Leonardo de Moura
d378df47d7
fix: fixes #633
2021-09-16 14:11:34 -07:00
Leonardo de Moura
04b7924154
chore: fix tests
2021-09-16 10:29:38 -07:00
Leonardo de Moura
1c00f29043
test: add let_fun pretty printing test
2021-09-16 10:14:42 -07:00
Leonardo de Moura
4c0ae51a81
chore: fix test
2021-09-16 10:13:34 -07:00
Leonardo de Moura
c2a5e37c60
feat: simp discharger
2021-09-16 10:11:27 -07:00
Leonardo de Moura
6fb2a2b47b
chore: remove ≅ notation for HEq
...
We don't really needed it here.
2021-09-15 08:06:32 -07:00
Leonardo de Moura
ae8989a8c6
feat: add mkAppOptM' and mkAppM'
2021-09-15 06:35:40 -07:00
Daniel Selsam
5eed3b73bf
chore: adjust pp.analyze funext test
2021-09-15 09:41:16 +02:00
Daniel Selsam
664737def8
feat: trust subtype.mk by default
2021-09-15 09:41:16 +02:00
Daniel Selsam
4b011affca
chore: better msgs in pp.analyze test
2021-09-15 09:41:16 +02:00
Daniel Selsam
4646b36459
feat: pp.analyze no explicit holes by default
2021-09-15 09:41:16 +02:00
Leonardo de Moura
db583550fd
feat: add Lean.Rat for implementing decision procedures
2021-09-14 19:18:12 -07:00
Leonardo de Moura
3fa54e604d
fix: inductive type name is not a necessarily a prefix of the constructor name in Lean 4 anymore
2021-09-14 18:52:43 -07:00
Leonardo de Moura
b92a2cd918
feat: heterogeneous congruence theorems
...
These theorems are needed to implement the congruence closure module.
2021-09-14 17:23:12 -07:00
Leonardo de Moura
deea3996be
fix: allow renameI to rename shadowed names
2021-09-13 06:43:34 -07:00
Leonardo de Moura
96d00ff2d7
fix: fixes #664
2021-09-12 19:54:45 -07:00
Leonardo de Moura
6a9ac6c484
test: rw without offset constraints modulo
2021-09-12 19:37:18 -07:00
Leonardo de Moura
bbe6d37109
fix: specialize
2021-09-11 19:52:51 -07:00
Leonardo de Moura
1fd3cfb19f
feat: pretty print let_fun
2021-09-11 05:15:11 -07:00
Leonardo de Moura
127681666a
test: more equality theorems using split
2021-09-10 19:36:27 -07:00
Leonardo de Moura
e667385cf5
feat: simpLet when zeta reduction is disabled
2021-09-10 19:34:38 -07:00
Leonardo de Moura
1e1a085ab3
test: eq theorem derivation
2021-09-09 17:51:49 -07:00
Leonardo de Moura
7607a24469
test: deriving DecidableEq for enum types
...
Forgot to add test.
2021-09-09 17:47:23 -07:00
Leonardo de Moura
09eecc5c08
fix: simp was not applying rewrites to the function application prefixes
2021-09-09 17:07:14 -07:00
Leonardo de Moura
5a7badd69a
feat: add support for erasing keyed attributes
...
This commit addresses any issue described at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Eq.2Endrec.20vs.20Eq.2Erec
2021-09-09 14:28:41 -07:00
Leonardo de Moura
4087525cba
feat: add delta tactic
2021-09-09 13:07:33 -07:00
Leonardo de Moura
193d4dc9f5
feat: optimized deriving DecidableEq for enumeration types
...
The proof term is liner on the number of constructors, but type
checking is not linear because the reduction engine in the kernel is
not efficient.
2021-09-08 16:21:32 -07:00
Leonardo de Moura
9b0dfc4b90
feat: convert "orphan" kernel nat literals n into ofNat n
2021-09-08 14:58:13 -07:00
