max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
27466 commits 1 branch 0 tags 5.3 GiB
Commit graph

80 commits

Author SHA1 Message Date
Leonardo de Moura
33883e9d2a fix: resulting type of projection functions should not include auxiliary type annotations (e.g., autoParam) 2022-03-10 07:47:38 -08:00
Leonardo de Moura
5825eb394f refactor: move isOutParam to Expr.lean, rename consumeAutoOptParam => consumeTypeAnnotations 2022-03-10 07:37:41 -08:00
Leonardo de Moura
164f07a5e5 feat: generalize Expr.abstractRange 
It now takes free variables **and** metavariables.
This is the first step to make `mkForallFVars` and `mkLambdaFVars`
more general.
 2022-03-08 18:19:17 -08:00
Leonardo de Moura
e574c5373f feat: improve delta? method 
Use zeta reduction to create new opportunities of beta-reduction.

This issue fixes on the problems that were affecting the generation of
equation theorems for `Array.heapSort.loop` (see issue: #998).
After this fix, the equation theorem generation fails at `splitMatch`.
 2022-02-09 13:31:55 -08:00
Leonardo de Moura
cf3b8d4eb4 chore: cleanup 
Make the code style more uniform.
We still have a lot of leftovers from the old frontend.
 2022-01-26 09:18:17 -08:00
Leonardo de Moura
763a337c25 chore: helper functions 2022-01-22 09:30:57 -08:00
Leonardo de Moura
0615020cf7 feat: make sure Expr.approxDepth does not overflow 2022-01-22 07:45:19 -08:00
Leonardo de Moura
b0083e0dd0 feat: use elaborated type to generate instance name 
closes #951
 2022-01-20 17:09:55 -08:00
Leonardo de Moura
b1a92f5cbf feat: better Repr instances for Level.Data and Expr.Data 
see #619
 2022-01-20 09:45:30 -08:00
Leonardo de Moura
ff4be1e1db feat: add Repr instances for Level and Expr 
closes #619

TODO: a better `Repr` instance for `Expr.Data`
 2022-01-20 09:26:06 -08:00
Leonardo de Moura
d782a97f5c feat: add WF.mkProof for WF.mkEqns 2022-01-04 17:00:54 -08:00
Leonardo de Moura
58430704e5 refactor: move inaccessible? to Expr.lean 2021-10-20 15:54:18 -07:00
Leonardo de Moura
db5df69db4 fix: bounds check 
fixes #704
 2021-09-30 07:55:10 -07:00
Leonardo de Moura
c53d892f22 feat: add Expr.projExpr! 2021-09-27 19:06:10 -07:00
Leonardo de Moura
f40a9b7912 feat: add consumeAutoOptParam 2021-09-14 16:09:46 -07:00
Leonardo de Moura
1fd3cfb19f feat: pretty print let_fun 2021-09-11 05:15:11 -07:00
Leonardo de Moura
445cc3085f refactor: avoid Name, MVarId, and FVarId confusion 2021-09-07 19:06:50 -07:00
Leonardo de Moura
1d68f38aa6 feat: use approxDepth to compute hash code 2021-09-06 07:36:41 -07:00
Leonardo de Moura
fa29428934 feat: use 8-bits to store the approximate depth on an expression 
We are going to use this information to (try to) minimize the number
of hash collisions.
 2021-09-06 07:26:51 -07:00
Leonardo de Moura
397774157f feat: nested tactic support in conv mode 2021-09-02 19:12:05 -07:00
Leonardo de Moura
391366ef24 refactor: add annotation for displaying conv state 2021-09-02 15:52:11 -07:00
Leonardo de Moura
fcbd807c9d chore: some Expr constructors 2021-08-16 13:58:48 -07:00
Leonardo de Moura
5ef72057e9 feat: save additional information at StructureFieldInfo 2021-08-09 19:01:08 -07:00
Leonardo de Moura
d1d7ce1839 feat: start support for strict implicit binder annotation 2021-08-03 18:42:15 -07:00
Leonardo de Moura
635bc78d72 feat: use structure extension to implement Structure.lean 2021-08-02 18:03:20 -07:00
Leonardo de Moura
bba9353619 fix: make sure isDefEqOffset does not expose kernel nat literals 
This issue is similar to a bug where `isDefEqOffset` was exposing
`Nat.add` when processing `HAdd.hAdd`.

Fixes #561
The example at issue #561 is now working, but we may have other places
where raw literals are being accidentally exposed.
 2021-08-02 11:27:00 -07:00
Leonardo de Moura
ad216db08d chore: add Repr instance for Literal and Key 2021-07-29 09:34:55 -07:00
Leonardo de Moura
7424f9c8b0 chore: remove HashableUSize 2021-06-02 09:58:46 -07:00
Leonardo de Moura
cbab9438c9 chore: Hashable instances for Expr and Level 2021-06-02 08:30:25 -07:00
Leonardo de Moura
43812444a7 chore: Hashable => HashableUSize 2021-06-02 07:24:26 -07:00
Leonardo de Moura
6a87bba9c0 chore: mixHash => mixUSizeHash 2021-06-02 07:05:42 -07:00
Leonardo de Moura
3a80e87793 chore: #405 step 1 2021-04-22 20:03:48 -07:00
Leonardo de Moura
f55561008c fix: fixes #386 2021-04-11 20:57:39 -07:00
Leonardo de Moura
642342d6c1 feat: add Expr.eta 2021-04-09 14:21:21 -07:00
Sebastian Ullrich
e62542ed29 feat: CoeSort Bool Prop 2021-03-20 14:52:16 +01:00
Leonardo de Moura
865316bbf9 feat: improve error message when stuck solving universe constraints 
closes #343
 2021-03-11 17:46:44 -08:00
Leonardo de Moura
fc79b794ba fix: missing error messages 
Issue reported by @JasonGross
 2021-03-05 17:20:04 -08:00
Leonardo de Moura
244b72befd feat: simpArrow 2021-01-01 17:15:15 -08:00
Leonardo de Moura
5f6e66a53f refactor: Repr 
Modifications:
- Result type is `Format`
- It takes the context precedence like Haskell `Show`
 2020-12-18 11:21:30 -08:00
Leonardo de Moura
0d9694d836 chore: user deriving BEq 2020-12-13 16:30:07 -08:00
Leonardo de Moura
15232f51d3 feat: add Expr.constainsFVar 2020-12-13 15:51:48 -08:00
Leonardo de Moura
04a07c15b9 chore: use deriving Inhabited 2020-12-13 11:57:59 -08:00
Leonardo de Moura
5249fdc24d chore: cleanup and style 2020-12-12 10:36:26 -08:00
Leonardo de Moura
7a4b544b1c feat: improve application type mismatch error message 
If the type error is at an implicit argument, we annotate
application with `pp.explicit := true`

Given the type incorrect definition
```
def f {a b c : α} : a = c :=
  Eq.trans (a := a) (b := b = c)
```
We now generate the error
```
error: application type mismatch
  @Eq.trans α a (b = c)
argument
  b = c
has type
  Prop
but is expected to have type
  α
```
@Kha Note that we only enable `pp.explicit := true` for the relevant
application. That is, we set `pp.explicit := false` for each children.

Unfortunately, there is a corner case.
```
set_option pp.explicit true
def f {a b c : α} : a = c :=
  Eq.trans (a := a) (b := b = c)
```
produces the error
```
error: application type mismatch
  @Eq.trans α a (b = c)
argument
  @Eq α b c
has type
  Prop
but is expected to have type
  α
```
The reset `pp.explicit := false` overwrote the user option.
I think the simplest solution is the following
1- The delaborator saves the initial set of Options `Init`
2- When it finds a node annotated with a `pp` options, it only
consider the option if it is not set by `Init`.

What do you think?
 2020-12-09 13:58:08 -08:00
Leonardo de Moura
0869f38de4 chore: update structure, class, inductive 2020-11-27 15:09:30 -08:00
Leonardo de Moura
d6f778bec4 refactor: arbitrary without explicit arguments 
@Kha I was tired of writing `arbitrary _` :)
There 0 places in the stdlib where the type needs to be provided.
If in the future we need to specify the type we can use
`arbitrary (α := <type>)`
 2020-11-25 09:07:38 -08:00
Leonardo de Moura
cb9574b086 chore: test unboundImplicitLocals and cleanup 2020-11-22 10:33:28 -08:00
Leonardo de Moura
8598dde6e6 fix: if-then-else elaboration issue 
@Kha I hate this kind of hack, but the behavior looked unacceptabled
to me. I added a big comment describing the issue and the hack.
 2020-11-21 20:51:28 -08:00
Leonardo de Moura
c305c2691f chore: use := 2020-11-19 07:22:31 -08:00
Leonardo de Moura
2daeb195b5 chore: use new names 2020-11-10 10:15:19 -08:00