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

2631 commits

Author SHA1 Message Date
Leonardo de Moura
a897fd3f17 fix(frontends/lean): pattern matching in the declaration header 2017-03-16 01:09:12 -07:00
Leonardo de Moura
36770119b6 feat(library): do not generate C.destruct (for structures), and C.induction_on (for structures and inductive datatypes) 2017-03-15 14:45:13 -07:00
Daniel Selsam
7f56f23e70 chore(frontends/lean/inductive_cmds): allow sorrys 2017-03-15 14:06:56 -07:00
Sebastian Ullrich
e3b9190fe2 refactor(library/tactic/user_attribute): use attribute for registering attributes. naturally. 2017-03-15 14:06:34 -07:00
Sebastian Ullrich
c325438453 fix(frontends/lean/elaborator): let expr patterns 2017-03-15 14:06:08 -07:00
Sebastian Ullrich
647d7a8501 fix(frontends/lean/elaborator): expr patterns should ignore binding names 2017-03-15 14:06:00 -07:00
Leonardo de Moura
9ce9c0331f feat(frontends/lean/elaborator): add option 'elaborator.coercion' 
This option is available in Lean 2, but it was accidentally removed
from Lean 3.
 2017-03-12 11:27:41 -07:00
Leonardo de Moura
bc7089dc70 chore(frontends/lean/elaborator): retract c58f61e 
See discussion at #1438
 2017-03-12 09:58:57 -07:00
Leonardo de Moura
c694dbd600 fix(frontends/lean/elaborator): conflict between (: t :) and (::) notations 
It was preventing us from using `(::)`
 2017-03-12 09:29:42 -07:00
Leonardo de Moura
9c24b81cbf feat(frontends/lean/elaborator): improve error message 2017-03-11 16:35:40 -08:00
Daniel Selsam
538ac8d187 feat(inductive_compiler): generate injectivity lemmas 2017-03-10 22:27:18 -08:00
Sebastian Ullrich
e3bfd90b06 fix(frontends/lean/elaborator): default recover_from_error to false for most commands 
Fixes #1446

fix(frontends/lean/util): quoting private name

uncovered by now failing run test
 2017-03-09 20:51:35 -08:00
Sebastian Ullrich
16558bf082 refactor(library,library): rename pre_monad to has_bind 2017-03-09 20:32:25 -08:00
Leonardo de Moura
9d3c0497cb chore(frontends/lean): rename transient commands 
See issue #1432
 2017-03-09 18:41:19 -08:00
Leonardo de Moura
a00f2e49a7 chore(frontends/lean): remove several command aliases 
We still have many more to remove and rename.
See issue #1432
 2017-03-09 16:49:03 -08:00
Leonardo de Moura
b6f6126075 feat(frontends/lean/pp): add attribute [pp_using_anonymous_constructor] for marking structures we should use the anonymous constructor notation when pretty printing instances 2017-03-09 15:17:18 -08:00
Leonardo de Moura
c58f61e925 feat(frontends/lean/elaborator): new encoding for structure updates {s with ...} 
See discussion at #1438
https://github.com/leanprover/lean/pull/1438#discussion_r105007325

@digama0 With this commit, the original `array_list.write` will also
perform a destructive update when the reference counter for `l` is 1.

```lean def write {α} (l : array_list α) : fin l^.length → α → array_list α :=
λ ⟨n, h⟩ v, { l with data := l^.data^.write ⟨n, l^.lt_capacity h⟩ h v }
```
 2017-03-09 00:11:51 -08:00
Leonardo de Moura
d775ee98b4 feat(frontends/lean): auto_param support at structure_instance, and better error messages 
Summary:

- A field value was being elaborated more than once when there is
  another field whose default value depends on it.
  The new test `structure_default_value_issue.lean` exposes the problem.

- Better error message and localization at field type mismatches.
  When there is field type mismatch, the error message contains the
  field name, and the error is reported at the field position instead of
  `{`.

- We add support for auto_param at structure instances `{...}`
  See #1422
 2017-03-08 18:04:36 -08:00
Leonardo de Moura
23935ee390 feat(frontends/lean): allow auto_param notation in structure declarations 
See #1422

TODO: take the auto_param into account in the `{ ... }` notation.
 2017-03-08 15:41:30 -08:00
Sebastian Ullrich
970e11bf5e feat(frontends/lean/{elaborator,structure_cmd}): allow overriding field defaults 2017-03-08 10:41:20 -08:00
Leonardo de Moura
8d3c7e7180 fix(frontends/lean/builtin_exprs): fixes #1433 2017-03-07 16:21:12 -08:00
Leonardo de Moura
51958df84b chore(frontends/lean/token_table): remove dead keywords 2017-03-07 14:00:49 -08:00
Leonardo de Moura
c427350dc0 chore(frontends/lean/token_table): remove dead commands 2017-03-07 13:50:14 -08:00
Daniel Selsam
7dcc36277a feat(frontends/lean/inductive_cmds.cpp): better resultant universe inference 2017-03-07 12:55:01 -08:00
Leonardo de Moura
f2faea9b9f refactor(frontends/lean/equations_validator): move validation code to another file 2017-03-06 14:36:42 -08:00
Daniel Selsam
5f0ebf90de fix(frontends/lean/structure_cmd): call inductive compiler without params in type 2017-03-06 14:01:46 -08:00
Sebastian Ullrich
2394f1faa5 fix(frontends/lean/util): do not fall back to current position 2017-03-06 11:02:51 -08:00
Sebastian Ullrich
c4ebfab14c fix(frontends/lean/structure_cmd): inheriting defaulted field depending on field starting with implicit parameter 2017-03-06 11:02:51 -08:00
Sebastian Ullrich
87b98d5aa2 fix(frontends/lean/structure_cmd): fix assertion violation when field depends on defaulted field 2017-03-06 11:02:50 -08:00
Daniel Selsam
ce1ec69ea6 fix(frontends/lean/decl_utils.cpp): closes #1417 2017-03-06 10:54:22 -08:00
Leonardo de Moura
045fe4ad25 fix(frontends/lean/structure_cmd): allow default values for function fields 2017-03-06 07:41:42 -08:00
Leonardo de Moura
61c9a7d466 feat(frontends/lean/elaborator): address issue described at https://github.com/leanprover/lean/issues/1403#issuecomment-282846138 
see #1403
 2017-03-05 21:01:12 -08:00
Leonardo de Moura
fa99861788 feat(frontends/lean/elaborator): add new ^. notation 
see #1403
 2017-03-05 20:12:49 -08:00
Sebastian Ullrich
876a2bee46 feat(frontends/lean/elaborator): flag expr quotes containing universe params 2017-03-05 08:37:16 -08:00
Sebastian Ullrich
5d68938a9c feat(frontends/lean): expr literals ```(...) 2017-03-05 08:37:16 -08:00
Leonardo de Moura
17556758cb feat(library/constructions,library/inductive_compiler): automatically generate dependent eliminator for inductive predicates 
The dependent eliminator for an inductive predicate C is called C.drec

TODO: construct dcases_on and drec_on using C.drec

We need this recursor for implementing dependent elimination for
inductive predicates.

We don't need to define acc.drec and eq.drec in the standard library anymore.
 2017-02-28 20:58:04 -08:00
Leonardo de Moura
1fa1312c57 chore(CMakeLists,frontends/lean): add SAVE_SNAPSHOT=OFF SAVE_INFO=OFF compilation options 2017-02-28 12:09:19 -08:00
Gabriel Ebner
fcc0f30b84 fix(frontends/lean/definition_cmds): set scope_pos_info when checking examples 2017-02-25 12:56:46 -08:00
Leonardo de Moura
52221cdbd1 fix(frontends/lean/elaborator): {} elaboration issue 2017-02-24 21:20:39 -08:00
Leonardo de Moura
552a185e6a feat(frontends/lean): 'let' in 'do' blocks 2017-02-24 09:10:36 -08:00
Sebastian Ullrich
dfe1874365 refactor(frontends/lean/{parser,util}): extract quote functions 
Also fixes ``f when f is private
 2017-02-23 01:52:13 +01:00
Sebastian Ullrich
1c7ca3f20a feat(frontends/lean/parser): ignore implicit arguments in expr patterns 2017-02-23 01:52:13 +01:00
Sebastian Ullrich
908a7bd9f3 feat(frontends/lean/parser): expr patterns 2017-02-23 01:52:13 +01:00
Leonardo de Moura
ca31ad0107 perf(library/metavar_util): quadratic behavior when assembling the final proof 
The peformance problem was affecting theorems that contain many `intro`
tactic applications.

@gebner After this optimization, the GAPT benchmark elaboration time went from
1.6 secs to 0.6 secs.
 2017-02-21 21:02:43 -08:00
Leonardo de Moura
622e9a6035 feat(library/type_context): use m_unfold_pred to decide whether macros should be unfolded or not 
see #1394
 2017-02-21 18:07:39 -08:00
Sebastian Ullrich
a053175714 refactor(init/meta,library/vm): use structure for position information 2017-02-21 11:06:39 -08:00
Leonardo de Moura
61254847fb fix(frontends/lean/structure_cmd): when error recovery is enabled, we must not assume the expression in the fixed line is a binding expression (it may be a sorry expression) 2017-02-20 14:51:59 -08:00
Leonardo de Moura
ddee94b831 fix(frontends/lean/elaborator): incorrect invariant due to error recovery 
We cannot assume both source and target are binding expressions.
The source has already been elaborated, and it may be a `sorry` because
of error recovery code.
 2017-02-20 14:30:10 -08:00
Leonardo de Moura
0d22410e2e feat(library/tactic): add zeta option, refactor simplify config option, allow users to change simplify_config in interactive mode 2017-02-19 12:11:22 -08:00
Leonardo de Moura
c065faaf1f feat(frontends/lean/elaborator): improve ^. notation 2017-02-18 16:20:21 -08:00