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

25274 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Wojciech Nawrocki
0b6d51d60b feat: tag pretty-printer outputs 2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
9b8e44618d chore: default to Format Nat 2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
a937fa26ba chore: fewer explicit types 2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
f51b80060d feat: generic tagged Format 2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
d2e23ff5cf fix: deriving RpcEncoding 2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
1d57ffb4d7 refactor: shuffle classes to avoid dependency loops 2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
1311f87a8b feat: eagerly initialize RPC session 
With this we are able to send RpcRefs immediately, in particular in (interactive) diagnostics.
 2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
d3ca1e98e9 refactor: make lsp/release a notification 2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
55ffb73bbe refactor: rename rpc/initialize to rpc/connect 2021-08-01 09:58:44 +02:00
Leonardo de Moura
af5ff9ceb2 refactor: move List.takeWhile to Init.Data.List.Basic 
Motivation: make sure it will be aligned by BinPort
 2021-07-31 15:03:33 -07:00
Leonardo de Moura
59dff3f3e0 chore: update stage0 2021-07-31 14:30:43 -07:00
Leonardo de Moura
3f72555437 feat: use staged sets at namespacesExt 
Mathlib has more than 120k namespaces
 2021-07-31 14:27:24 -07:00
Leonardo de Moura
6cc30a3f90 feat: add NameSSet 
Staged set of names
 2021-07-31 14:24:00 -07:00
Leonardo de Moura
2abafd9df4 feat: add "staged set" helper type 2021-07-31 14:23:29 -07:00
Leonardo de Moura
bd60e59f9a feat: add HashMap.insert' 
The new function returns a flag indicating whether the new entry
replaced an existing or not.
We use it to implement `importModules`.
 2021-07-31 13:42:01 -07:00