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

5716 commits

Author SHA1 Message Date
Sebastian Ullrich
e76fc17b0e fix: rw goal state positions 2021-05-03 14:14:12 +02:00
Sebastian Ullrich
4fb01f7c06 fix: goal state on ; 2021-05-03 13:32:00 +02:00
Leonardo de Moura
e5083f2521 fix: avoid unnecessary unfolding at do 2021-05-02 21:29:32 -07:00
Leonardo de Moura
d556ebbdc6 test: add test for binder caching issue 2021-05-02 20:04:41 -07:00
Leonardo de Moura
56c7454a8d fix: fixes #435 2021-05-02 18:16:57 -07:00
Leonardo de Moura
0f8c6ca797 fix: cache issue at instantiateBetaRevRange 2021-05-02 17:00:35 -07:00
Leonardo de Moura
78a2de4241 feat: better error recovery for match syntax 2021-05-02 17:00:35 -07:00
Sebastian Ullrich
b8b8cc79a9 feat: show initial case goal on ... => for induction/cases/case/match 2021-05-02 23:07:15 +02:00
Sebastian Ullrich
8863761401 feat: show initial state for tactic combinators by default 2021-05-02 23:07:15 +02:00
Sebastian Ullrich
2734a5baba feat: show state on by 2021-05-02 23:07:15 +02:00
Leonardo de Moura
1a0fc816b1 feat: rename inaccessible variable names at cases 2021-05-01 21:51:58 -07:00
Leonardo de Moura
a2e8bc0780 feat: use binop% to define arith operators 
closes #382
 2021-04-30 19:40:45 -07:00
Leonardo de Moura
a04babf263 chore: fix tests affected by recent changes 2021-04-30 19:37:18 -07:00
Sebastian Ullrich
e1cde87c43 fix: server: completion & goal state at EOF 2021-04-30 19:25:53 +02:00
tydeu
44f45f426c
feat: add scoped macro_rules (#432) 2021-04-30 09:05:09 +02:00
Leonardo de Moura
adae6fdb40 fix: tolerate type incorrect terms 
This bug was producing a type error when I was using `set_option trace.Elab true`
 2021-04-29 21:34:15 -07:00
Sebastian Ullrich
f0960b7f89 fix: ignore antiquotations outside quotations 2021-04-29 13:33:48 +02:00
Sebastian Ullrich
683ecb2d65 feat: ignore unquoted identifiers in prechecked quotations 2021-04-29 13:30:09 +02:00
Leonardo de Moura
45bcf4a32c feat: check instance implicit binder annotations 2021-04-28 17:15:08 -07:00
Sebastian Ullrich
75e95f93a9 feat: improve let error locality 2021-04-27 16:38:46 -07:00
Sebastian Ullrich
9f0fa19237 feat: notation: unfold to prechecked quotation 2021-04-27 16:38:37 -07:00
Sebastian Ullrich
9301e05a7e feat: double-quoted quotation semantics and basic precheck hooks 2021-04-27 16:38:37 -07:00
Leonardo de Moura
35411d5b2c chore: fix tests 2021-04-27 16:06:26 -07:00
Leonardo de Moura
18085b9712 fix: improve match generalizing feature 2021-04-26 19:22:03 -07:00
Daniel Fabian
1f05f5bf11 chore: rename ProofBelow to below. 2021-04-26 20:33:21 +02:00
Sebastian Ullrich
14c5ec559b test: forgot tabs ban test 2021-04-26 17:09:48 +02:00
Leonardo de Moura
af391fe812 test: reflective inductive predicate 2021-04-25 20:35:13 -07:00
Daniel Fabian
eda4bdd337 test: extend inductive_pred.lean with tests using the new construction. 2021-04-25 20:02:22 -07:00
Leonardo de Moura
2cbdd637c7 test: add second example for issue #423 2021-04-25 10:35:23 -07:00
Leonardo de Moura
b670d6b8d7 test: for issue #423 2021-04-25 10:30:26 -07:00
Leonardo de Moura
0533fc4056 chore: fix test 2021-04-25 10:25:35 -07:00
Leonardo de Moura
f47f605039 fix: remove incorrect test 
It had two problems:
- It was preventing coercions from being applied.
- It was compromising error recovery. The body of the lambda was not
being elaborated when the exception was thrown.

The new error message is more verbose and potentially confusing, but
it is better than the one produced this morning.
 2021-04-24 22:17:29 -07:00
Leonardo de Moura
1f9975d35d feat: improve error message and include variables introduced by the implicit lambda notation 2021-04-24 21:34:42 -07:00
Leonardo de Moura
10185d24dd feat: improve error message 2021-04-24 20:43:13 -07:00
Leonardo de Moura
a6888f72dd fix: instance + where + implicts issue 
The following could not be elaborated.

```lean
instance : MulComm Bool where
  mulComm := fun {a b} =>
    match a, b with
    | true, true   => rfl
    | true, false  => rfl
    | false, true  => rfl
    | false, false => rfl
```
 2021-04-24 20:07:35 -07:00
Leonardo de Moura
c76820a251 fix: no method lift over let 2021-04-24 19:33:55 -07:00
Leonardo de Moura
a076b5b89e feat: improved error recovery for interpolated strings 2021-04-24 10:24:57 -07:00
Leonardo de Moura
74d613ab88 fix: safe instance for MethodsRef 2021-04-24 07:24:08 -07:00
Leonardo de Moura
b2190da468 feat: add Macro.resolveGlobalName and Macro.resolveNamespace? 2021-04-23 19:38:56 -07:00
Leonardo de Moura
d70f9c232c feat: trace support for MacroM 
closes #184
 2021-04-23 19:15:14 -07:00
Leonardo de Moura
030f53fa43 fix: closes #421 
The unifier used to implement the `cases` tactic should not discard
equations of the form `x = t` and `t = x` using proof irrelanvance.
The new test demonstrates the issue. The unifier was reaching the
state
```
x : Conw Con.nil
|- x = Conw.nilw -> x = Conw.nilw
```
and discarding the equality instead of substituting `x`
because `x` and `Conw.nilw` are definionally equal due to
proof irrelevance.

@javra Do you have more complicated examples that were being
affected by this issue?
 2021-04-23 12:27:39 -07:00
Sebastian Ullrich
ccb873cea2 fix: panic on variable : 2021-04-23 09:24:35 +02:00
Sebastian Ullrich
8895ed47e5 refactor: clean up Thunk 
Fixes a bug in the native implementation of `Thunk.bind` by deleting it
 2021-04-22 20:29:08 -07:00
Leonardo de Moura
964fd3f520 chore: fixes tests 
closes #405
 2021-04-22 20:22:43 -07:00
Leonardo de Moura
e6e12ca408 fix: fixes #408 2021-04-22 19:07:03 -07:00
Leonardo de Moura
cebc301c11 chore: remove old test 2021-04-22 18:14:18 -07:00
Leonardo de Moura
09d438ca1d chore: enforce notation parameter naming convention 2021-04-19 18:54:09 -07:00
Leonardo de Moura
762cebbbfc fix: match generalization bug 2021-04-19 18:37:25 -07:00
Leonardo de Moura
aaca889bea fix: fixes #414 2021-04-19 15:02:26 -07:00
Leonardo de Moura
1dca9d18d4 fix: missing tactic state info on broken proofs 2021-04-18 20:13:02 -07:00