Daniel Selsam
cded8be388
feat: more HBinOps in pp.analyze
2021-08-03 09:13:18 +02:00
Daniel Selsam
54146f1859
fix: 4-ary SubExpr repr for types
2021-08-03 09:13:18 +02:00
Daniel Selsam
ce64629d63
chore: two comments about bad pp.analyze behavior
2021-08-03 09:13:18 +02:00
Daniel Selsam
9744b51c1b
fix: unexpand pairs
2021-08-03 09:13:18 +02:00
Daniel Selsam
3309da8f1e
fix: pp.analyze LocalInstances not in MessageData
2021-08-03 09:13:18 +02:00
Daniel Selsam
45a880ac05
feat: pp.analyze treat original uvars as params
2021-08-03 09:13:18 +02:00
Daniel Selsam
ca73f60894
feat: pp.analyze flag to trust ofScientific
2021-08-03 09:13:18 +02:00
Daniel Selsam
ff4551d217
fix: pp.analyze bottom up with fvar app-fns
2021-08-03 09:13:18 +02:00
Daniel Selsam
3b3e54143c
feat: pp.analyze isSubstLike support Eq.rec
2021-08-03 09:13:18 +02:00
Daniel Selsam
7030eaad3d
feat: one more pp.analyze pass
2021-08-03 09:13:18 +02:00
Daniel Selsam
d6412b3a98
fix: pp.analyze was still printing inaccessibles
2021-08-03 09:13:18 +02:00
Daniel Selsam
912e5cf212
fix: avoid pp.analyze trace/exception loop
2021-08-03 09:13:18 +02:00
Daniel Selsam
aa590ccdf5
feat: pp option to instantiate mvars
2021-08-03 09:13:18 +02:00
Daniel Selsam
b3bb82ee7e
feat: turn more delaborators into unexpanders
2021-08-03 09:13:18 +02:00
Daniel Selsam
0b19f8e5a5
fix: do not double @@
2021-08-03 09:13:18 +02:00
Daniel Selsam
2f9963f092
fix: literals are bottom-up safe
2021-08-03 09:13:18 +02:00
Daniel Selsam
a96a043618
feat: better coe support
2021-08-03 09:13:18 +02:00
Daniel Selsam
ca3be9876e
feat: flag to trust coercions
2021-08-03 09:13:18 +02:00
Daniel Selsam
50d67e77ac
fix: type ascriptions
2021-08-03 09:13:18 +02:00
Daniel Selsam
9158899145
feat: pp.analize try/catch and trace
2021-08-03 09:13:18 +02:00
Daniel Selsam
eed0fb6635
feat: special support for 'fun x => x'
2021-08-03 09:13:18 +02:00
Daniel Selsam
811bb56d10
fix: never set a negation
2021-08-03 09:13:18 +02:00
Daniel Selsam
548bf4d9f4
chore: rm stale todo
2021-08-03 09:13:18 +02:00
Daniel Selsam
4a35cef2c2
chore: rm stale instance
2021-08-03 09:13:18 +02:00
Daniel Selsam
e84a5ac432
fix: @ when there are inaccessible names
2021-08-03 09:13:18 +02:00
Daniel Selsam
280a3db653
fix: only print named patterns inside patterns
2021-08-03 09:13:18 +02:00
Daniel Selsam
d2ff2de4f6
feat: add @ to consts/locals with pi {..} type
2021-08-03 09:13:18 +02:00
Daniel Selsam
1c6cdceb64
refactor: simplify pp.analyze options
2021-08-03 09:13:18 +02:00
Daniel Selsam
6940166db4
chore: rebase and rm rawPos
2021-08-03 09:13:18 +02:00
Daniel Selsam
89364b802b
feat: top-down heuristic delaboration
2021-08-03 09:13:18 +02:00
Leonardo de Moura
ea37a29e4c
chore: remove TODO
2021-08-02 20:25:29 -07:00
Leonardo de Moura
50ae3d8e61
chore: update stage0
2021-08-02 20:23:56 -07:00
Leonardo de Moura
d864afae91
feat: private fields
...
closes #418
2021-08-02 20:20:21 -07:00
Leonardo de Moura
cfa086a471
chore: update stage0
2021-08-02 19:03:04 -07:00
Leonardo de Moura
90047e73e8
feat: cache structure parent names
2021-08-02 18:58:00 -07:00
Leonardo de Moura
694bed5b0b
chore: update stage0
2021-08-02 18:55:41 -07:00
Leonardo de Moura
cfb7e27b87
fix: isStructure vs isStructureLike
2021-08-02 18:54:19 -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
bdc6bc6fcc
chore: update stage0
2021-08-02 16:19:13 -07:00
Leonardo de Moura
1ca62e21fd
feat: add environment extension for storing structure field information
2021-08-02 16:17:35 -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
9e4582a7d0
fix: fixes #593
2021-08-02 10:46:12 -07:00
Leonardo de Moura
89e333ab52
chore: move import Lean.Elab.Open
2021-08-02 10:13:35 -07:00
Sebastian Ullrich
0db80c6ea8
chore: Nix: link with gold instead of lld
...
https://twitter.com/derKha/status/1419645259894640645
2021-08-02 13:42:11 +02:00
Leonardo de Moura
45b599ef69
chore: update stage0
2021-08-01 11:46:40 -07:00
Leonardo de Moura
6e9afe1b3d
feat: refine tryResolveCore
...
We need this refinement to be able to process the following example.
```
import Mathlib.RingTheory.Nullstellensatz
import Mathlib.PostPort.Coe
namespace MvPolynomial.Fun
open Ideal
variable {k : Type u} [instField : Field k]
variable {σ : Type v}
variable [instIAC : IsAlgClosed k] [instF : Fintype σ]
(@Ideal.{max v u}
(@MvPolynomial.{v, u} σ k
(@CommRingS.toCommSemiring.{u} k
(@EuclideanDomain.toCommRing.{u} k (@Field.toEuclideanDomain.{u} k instField))))
(@RingS.toSemiring.{max v u}
(@MvPolynomial.{v, u} σ k
(@CommRingS.toCommSemiring.{u} k
(@EuclideanDomain.toCommRing.{u} k (@Field.toEuclideanDomain.{u} k instField))))
(@Domain.toRing.{max v u}
(@MvPolynomial.{v, u} σ k
(@CommRingS.toCommSemiring.{u} k
(@EuclideanDomain.toCommRing.{u} k (@Field.toEuclideanDomain.{u} k instField))))
(@IntegralDomain.toDomain.{max v u}
(@MvPolynomial.{v, u} σ k
(@CommRingS.toCommSemiring.{u} k
(@EuclideanDomain.toCommRing.{u} k (@Field.toEuclideanDomain.{u} k instField))))
(@MvPolynomial.integralDomain.{u, v} k σ (@Field.toIntegralDomain.{u} k instField))))))
```
This example was extracted from a failure at
```
theorem vanishing_ideal_zero_locus_eq_radical (I : Ideal (MvPolynomial σ k)) : vanishingIdeal (ZeroLocus I) = I.radical
```
2021-08-01 11:42:39 -07:00
Leonardo de Moura
27fd35148c
refactor: dependent instances annotations
2021-08-01 10:58:22 -07:00
Wojciech Nawrocki
f1b4d9a193
chore: restore non-generic Format
...
Motivation: it is unclear whether this is the best solution for embedding objects in pretty-printer outputs.
2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
b022a7c1d2
style: indent
2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
5f021baa95
style: statement ordering
...
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
2021-08-01 09:58:44 +02:00
