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

75 commits

Author SHA1 Message Date
Leonardo de Moura
fa943d3864 chore: update RELEASES.md 2022-04-29 15:59:34 -07:00
Leonardo de Moura
0c8a6d8977 feat: exists es:term,+ tactic 
cc: @fgdorais
 2022-04-25 15:35:31 -07:00
Leonardo de Moura
47b379e1bc feat: dsimp! tactic 2022-04-23 18:41:04 -07:00
Leonardo de Moura
e25a116821 chore: RELEASES.md 2022-04-23 12:16:36 -07:00
Leonardo de Moura
66c82dadc9 fix: the default value for structure fields may now depend on the structure parameters 2022-04-21 17:38:19 -07:00
Leonardo de Moura
d1f10a2e71 feat: apply rfl theorems at dsimp 
closes #1113
 2022-04-21 16:26:57 -07:00
Leonardo de Moura
0b92195ec8 feat: refine auto bound implicit feature 2022-04-21 10:17:15 -07:00
Leonardo de Moura
4727fd6883 feat: do not hightlight auxiliary declarations used to compile recursive definitions as variables 
They are "morally" constants.
 2022-04-21 08:11:22 -07:00
Leonardo de Moura
556ace5cc1 chore: update RELEASES.md 2022-04-18 17:03:01 -07:00
Leonardo de Moura
4848ad4869 feat: implement autoUnfold at simp 
Right now, it only supports the following kind of definitions
- Recursive definitions that support smart unfolding.
- Non-recursive definitions where the body is a match-expression. This
kind of definition is only unfolded if the match can be reduced.
 2022-04-18 16:51:52 -07:00
Leonardo de Moura
40129203b2 chore: update RELEASES.md 2022-04-17 13:55:46 -07:00
Leonardo de Moura
f875c2d107 chore: update release notes 2022-04-13 10:33:25 -07:00
Leonardo de Moura
3d9439f3c9 chore: missing annotation 2022-04-13 09:03:58 -07:00
Leonardo de Moura
9126d33dda doc: update release notes 2022-04-13 09:01:55 -07:00
Leonardo de Moura
8b53cc8dbb chore: update RELEASES.md 2022-04-09 15:39:40 -07:00
Sebastian Ullrich
4aed79a13e feat: less strict, hopefully more helpful syntax ident matching semantics 2022-04-08 15:53:58 +02:00
Sebastian Ullrich
24697026e8 feat: always accept antiquotations, simplify quotDepth code 2022-04-06 19:43:07 +02:00
Leonardo de Moura
5470100830 feat: better binder names at reorderCtorArgs 2022-04-03 10:03:47 -07:00
Leonardo de Moura
3ee8ceafb4 feat: better error message when constructor parameter universe level is too big 2022-04-03 08:37:38 -07:00
Leonardo de Moura
64cfbc1ae3 feat: add helper tactic for applying sizeOf (a.get i) < sizeOf a automatically in termination proofs 2022-04-02 18:29:41 -07:00
Leonardo de Moura
2c7c7471db feat: add case' tactic for writing macros 
It is similar to `case` but does not admit goal in case of failure.
This is useful for writing macros.
 2022-04-02 17:54:06 -07:00
Leonardo de Moura
9f29d7ecb7 feat: add stop tactic macro 2022-04-02 15:39:03 -07:00
Leonardo de Moura
9fe5458077 feat: do not display inaccessible proposition names if they do not have forward dependencies 
Even if `pp.inaccessibleNames = true`
 2022-04-02 13:15:17 -07:00
Leonardo de Moura
e058fe65a9 feat: make the hypothesis name optional in the by_cases tactic 2022-04-01 19:36:13 -07:00
Leonardo de Moura
d473cc5a4c chore: update release notes for issue #1090 
closes #1090
 2022-04-01 11:38:50 -07:00
Leonardo de Moura
4c9c62752e feat: improve checkpoint tactic 2022-03-31 20:51:53 -07:00
Leonardo de Moura
3dd0c84c4d chore: enforce naming convetion for tactics 2022-03-30 16:19:05 -07:00
Leonardo de Moura
46ce3013d0 feat: cleanup local context before elaborating match alternatives RHS 2022-03-29 18:52:07 -07:00
Leonardo de Moura
86432f1833 feat: improve let-pattern and have-pattern macro expansion 2022-03-29 07:33:22 -07:00
Sebastian Ullrich
bef34e30e7 feat: Nix: render examples using LeanInk+Alectryon 2022-03-26 22:50:04 +01:00
Sebastian Ullrich
7ce5b0c4ff feat: CI: build darwin_aarch64 2022-03-26 16:29:52 +01:00
Sebastian Ullrich
2740cab3fc
chore: update RELEASES 2022-03-26 00:02:13 +01:00
Leonardo de Moura
9aca413e31 chore: add link to doc/examples 2022-03-25 14:46:43 -07:00
Leonardo de Moura
be7c71d1c8 chore: update date 2022-03-23 07:44:15 -07:00
Leonardo de Moura
321d6b0e67 feat: support for user-defined simp attributes in the simp tactic. 
See `RELEASES.md`

TODO: make sure `-thm` also removes `thm` from user-defined simp attributes.
 2022-03-20 18:45:57 -07:00
Leonardo de Moura
6d926c7989 feat: macro expand match alternatives 
see #371

This commit does not implement all features discussed in this issue.
It has implemented it as a macro expansion. Thus, the following is
accepted
```lean
inductive StrOrNum where
  | S (s : String)
  | I (i : Int)

def StrOrNum.asString (x : StrOrNum) :=
  match x with
  | I a | S a => toString a
```
It may confuse the Lean LSP server. The `a` on `toString` shows the
information for the first alternative after expansion (i.e., `a` is an `Int`).
After expansion, we have
```
def StrOrNum.asString (x : StrOrNum) :=
  match x with
  | I a => toString a
  | S a => toString a
```
 2022-03-20 14:20:13 -07:00
Sebastian Ullrich
4fd520e902 feat: generalize inferred namespace notation to functions 2022-03-16 23:40:05 +01:00
Leonardo de Moura
231120c118 chore: update RELEASES.md 2022-03-12 20:02:39 -08:00
Leonardo de Moura
cf0ca026fb feat: equation theorems at rw 2022-03-12 13:53:02 -08:00
Leonardo de Moura
15e30a93f3 feat: update RELEASES.md 2022-03-11 16:28:01 -08:00
Leonardo de Moura
ddf93d2f8a feat: support for arrow types in the dot notation 
cc @gebner
 2022-03-11 15:39:41 -08:00
Leonardo de Moura
2364bc7b46 chore: add link to issue 2022-03-10 17:10:12 -08:00
Leonardo de Moura
002412e9d0 chore: missing code block annotation 2022-03-10 17:08:54 -08:00
Leonardo de Moura
e1fa9c131c feat: inferring namespace from expected type a la Swift 
Now that `PatternVars.lean` has been redesigned, it is feasible to
implement issue #944.

closes #944
 2022-03-10 16:55:25 -08:00
Leonardo de Moura
3214a20d33 feat: allow overloaded notation in patterns 2022-03-10 12:51:34 -08:00
Leonardo de Moura
c1b1a916eb doc: update release notes 2022-03-10 08:26:27 -08:00
Leonardo de Moura
4ee131981d feat: in an inductive family the longest fixed prefix of indices is now promoted to parameters 
This modification is relevant for fixing regressions on recent changes
to the auto implicit behavior for inductive families.

The following declarations are now accepted:
```lean
inductive HasType : Fin n → Vector Ty n → Ty → Type where
  | stop : HasType 0 (ty :: ctx) ty
  | pop  : HasType k ctx ty → HasType k.succ (u :: ctx) ty

inductive Sublist : List α → List α → Prop
  | slnil : Sublist [] []
  | cons l₁ l₂ a : Sublist l₁ l₂ → Sublist l₁ (a :: l₂)
  | cons2 l₁ l₂ a : Sublist l₁ l₂ → Sublist (a :: l₁) (a :: l₂)

inductive Lst : Type u → Type u
  | nil  : Lst α
  | cons : α → Lst α → Lst α
```

TODO: universe inference for `inductive` should be improved. The
current approach is not good enough when we have auto implicits.

TODO: allow implicit fixed indices that do not depend on indices that
cannot be moved to become parameters.
 2022-03-08 17:56:34 -08:00
Sebastian Ullrich
dca5da6b18 chore: update RELEASES.md 2022-03-07 17:28:51 +01:00
Leonardo de Moura
d9a6680536 doc: describe the auto implicit chaining in the release notes 2022-03-05 17:45:56 -08:00
Leonardo de Moura
22731c02b0 fix: auto implicit locals in inductive families 2022-03-05 15:47:20 -08:00