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

27562 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
8f4d58893f feat: update match parser 
Support for
```
def fib (x : Nat) : Nat :=
  match x with
  | 0 | 1 => 1
  | x+2   => fib (x+1) + fib x
```

TODO: expand `matchAlts`
 2022-03-20 13:22:39 -07:00
Leonardo de Moura
87bb299f08 feat: add Iterator.atEnd 2022-03-20 11:40:46 -07:00
Leonardo de Moura
4f9dcd55ce chore: update stage0 2022-03-20 10:59:21 -07:00
Leonardo de Moura
3862e7867b refactor: make String.Pos opaque 
TODO: this refactoring exposed bugs in `FuzzyMatching` and `Lake`

closes #410
 2022-03-20 10:47:13 -07:00
Jakob von Raumer
a91f92c11e feat: allow constants to be type classes 
There no reason against constants to be type classes so it is just the check in `addClass` that is needed to be modified.

Closes #1054
 2022-03-20 08:03:34 -07:00
Leonardo de Moura
6e94801c00 chore: update stage0 2022-03-19 16:55:26 -07:00
Leonardo de Moura
1b357db3b0 fix: nasty bug at findDeclarationRangesCore? 
We must search the environment extension first, and then the builtin
table. Otherwise, the builtin declarations do not change when we
modify the files.

closes #1021
 2022-03-19 16:53:22 -07:00
Leonardo de Moura
ed7c8904a9 fix: propagate local and scope modifiers at elab_rules 
closes #1039
 2022-03-19 16:08:06 -07:00
Leonardo de Moura
82cd5c8eef chore: cleanup 2022-03-19 15:52:04 -07:00
E.W.Ayers
da68f629f9 style: Apply.lean 
Apply Leo's review requests.
 2022-03-19 15:51:40 -07:00
E.W.Ayers
d954706fcf feat: ApplyNewGoals config for apply 
Lean.Meta.Tactic.apply now accepts an ApplyConfig argument.
`apply` now changes which metavariables are stored with choice
of the newGoals config.
This allows one to implement `fapply` and `eapply`.
An example of this is given in tests/lean/run/apply_tac.lean.

Closes #1045
 2022-03-19 15:51:40 -07:00
casavaca
bf4ba1583d feat: add simp theorem for List, (as.map f).length = as.length 2022-03-19 11:35:21 -07:00
Leonardo de Moura
72b6f4d528 chore: avoid unnecessary h :s 2022-03-19 11:21:37 -07:00
Leonardo de Moura
f29319647f chore: update stage0 2022-03-19 11:16:24 -07:00
Leonardo de Moura
4f318d3304 test: use dot notation in the example 2022-03-19 10:39:58 -07:00
Leonardo de Moura
d1eb180aae test: add non mutually recursive version 2022-03-19 10:38:39 -07:00
Leonardo de Moura
bdb2e9597a chore: naming convention 2022-03-19 10:20:42 -07:00
Leonardo de Moura
6c8322d20a test: use builtin Char.isDigit and Char.toNat 2022-03-19 10:18:34 -07:00
Leonardo de Moura
a8ddb56e0e chore: cleanup David's example 2022-03-19 10:13:27 -07:00
Leonardo de Moura
c95d5f25a3 feat: convert ites into dites in the WF module 
Motivation: the condition is often used in termination proofs.
 2022-03-19 10:11:50 -07:00
Leonardo de Moura
9fed5bda7d chore: remove workarounds 2022-03-19 09:44:57 -07:00
Leonardo de Moura
544421faf5 chore: update stage0 2022-03-19 09:43:57 -07:00
Leonardo de Moura
36d955e8cc feat: use simpler encoding for nonmutually recursive definitions 2022-03-19 09:43:18 -07:00
Leonardo de Moura
4b374d4441 fix: Nat/Div.lean, add decreasing_with combinator, and rename decreasing_tactic_trivial 2022-03-19 09:40:10 -07:00
Leonardo de Moura
5e3b3494e2 chore: update stage0 2022-03-19 09:30:34 -07:00
Leonardo de Moura
c7cdbf8ff8 feat: improve auto generated termination_by a bit 2022-03-19 09:28:19 -07:00
Leonardo de Moura
64c5cda612 test: David's lex with string iterators 2022-03-19 09:15:29 -07:00
Leonardo de Moura
9722aeaf32 feat: use String.Iterator.sizeOf_next_lt in the builtin decreasing_tactic 2022-03-19 09:04:40 -07:00
Leonardo de Moura
7dd38a7194 feat: add with_unfolding_all and rfl' tactics 2022-03-19 08:57:04 -07:00
Leonardo de Moura
63e42a8179 chore: fix copyright date 
File was created in 2022.
 2022-03-19 08:44:21 -07:00
Leonardo de Moura
c8c4d47420 feat: make decreasing_tactic easier to extend 2022-03-19 08:42:38 -07:00
Leonardo de Moura
ef3143e1eb chore: update stage0 2022-03-19 08:39:34 -07:00
Leonardo de Moura
fa74194638 fix: missing s.restore at expandTacticMacroFns 2022-03-19 08:34:54 -07:00
Leonardo de Moura
bd7827ed04 feat: dbg_trace tactic for low-level tactic debugging 2022-03-19 08:25:49 -07:00
Leonardo de Moura
9727387129 feat: helper theorem for proving termination of simple String traversal functions 2022-03-19 07:37:59 -07:00
Leonardo de Moura
ed3c792a4c chore: update stage0 2022-03-19 07:21:52 -07:00
Leonardo de Moura
64bd82dddd feat: custom SizeOf instance for String.Iterator 2022-03-19 07:21:17 -07:00
Leonardo de Moura
4ac88d0eb8 test: lex example from David 2022-03-18 19:53:17 -07:00
Leonardo de Moura
a486503c62 chore: fold Nat literals at reduce 2022-03-18 17:10:46 -07:00
Leonardo de Moura
1514e39006 chore: add double ticks 2022-03-18 17:10:46 -07:00
Leonardo de Moura
42b707e250 perf: improve getMatchWithExtra 2022-03-18 17:10:46 -07:00
Sebastian Ullrich
d5b3430e53 chore: ignore stage0/ (for rg etc.) 2022-03-18 15:28:20 +01:00
Leonardo de Moura
38a1675c72 fix: dicrimination tree getMatchWithExtra 
It was buggy when the input argument could be reduced `e`.

fixes #1048
 2022-03-17 16:44:38 -07:00
Leonardo de Moura
3193acecfa fix: flush the CoreM and MetaM caches at modifyEnv 
This fix may impact performance. Note that we don't need to flush the
cache if we are "adding" stuff to the environment. We only need to
flush the caches if the change is not monotonic. BTW, most of the
changes are monotonic. I think this is why we did not hit this bug before.

We may also move all these caches to an environment extension. It is
an easy way to make sure we preserve the cache when extending the
environment.

I tried a few benchmarks and did not notice a significant difference.

cc @kha @gebner

fixes #1051
 2022-03-17 16:02:30 -07:00
Leonardo de Moura
719db55a9c chore: fix trace class 2022-03-17 13:22:16 -07:00
Leonardo de Moura
184b0b8e8d feat: improve "result types must be in the same universe level" error message 
The new error message makes it clear why the definition is not accepted.

See issue #1050
 2022-03-17 07:41:37 -07:00
zygi
ac793ce196 fix: forward start and stop in Array.allM 2022-03-17 10:08:40 +01:00
Sebastian Ullrich
0d03c6e319 chore: revise non-GMP interface 2022-03-16 17:32:51 -07:00
Daniel Fabian
969eea19f0 refactor: do not use mkAppM so much 2022-03-16 17:21:20 -07:00
Daniel Fabian
cf4e873974 feat: support Sort u in ac_refl. 2022-03-16 17:21:20 -07:00