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

1677 commits

Author SHA1 Message Date
Leonardo de Moura
87932f1c56 feat(frontends/lean): change notation for inaccessible patterns 
The following are accepted
 .(t)
 ._

We don't accept .t anymore because it will conflict with the field
access notation.
 2017-03-28 16:09:15 -07:00
Leonardo de Moura
8e2dcb8ad8 chore(frontends/lean): remove ^. variants (~> and ↣) 
This modification was motivated by a discussion at slack.
 2017-03-28 12:23:33 -07:00
Leonardo de Moura
092985f777 fix(frontends/lean/util): fixes #1495 
We should freeze only constants
 2017-03-28 11:55:11 -07:00
Leonardo de Moura
9a4e04b8ca feat(frontends/lean/structure_cmd): add equational lemma for auxiliary default values 2017-03-27 21:37:31 -07:00
Leonardo de Moura
71bf0bcc5d fix(frontends/lean/builtin_exprs): fixes #1493 2017-03-27 17:57:13 -07:00
Leonardo de Moura
1cef8af1be feat(library/tactic/simplify): add eta := tt to simp 2017-03-27 17:38:40 -07:00
Leonardo de Moura
eea46610ea fix(library/tactic/simplify): missing projection reduction, add proj := tt to simp 2017-03-27 17:38:40 -07:00
Leonardo de Moura
161879b1bf feat(library/init/meta): add helper tactic guard_target for generating tests 2017-03-27 17:38:40 -07:00
Leonardo de Moura
b09968a37b feat(library/tactic/simplify): add beta := tt to simp 2017-03-27 17:38:31 -07:00
Leonardo de Moura
494e5b65c5 feat(library/init/meta/tactic): add apply_auto_param and apply_opt_param tactics 
see #1485
 2017-03-27 13:42:08 -07:00
Leonardo de Moura
e98f69d1ac fix(frontends/lean/elaborator): ignore auto/default params when @ is used 
see #1485

@kha We need this commit to be able to execute commands such as:
```lean
  #check @monad.mk
```
 2017-03-27 13:42:08 -07:00
Sebastian Ullrich
c7b47c7b7f fix(system/io): try to fix io monad 2017-03-27 13:42:08 -07:00
Sebastian Ullrich
dfd84666e2 feat(library): add functor, applicative, and monad laws, and prove them correct for non-meta instances 2017-03-27 13:42:08 -07:00
Leonardo de Moura
8cf43e1b30 feat(library/tactic/tactic_state): add tactic.run_io 2017-03-23 18:17:53 -07:00
Leonardo de Moura
fe3875a103 feat(library/system/io): add stdin, stdout and stderr 2017-03-23 16:49:39 -07:00
Leonardo de Moura
82748a61b7 feat(library/system/io): basic file system API 2017-03-23 16:30:16 -07:00
Leonardo de Moura
527c8851a8 refactor(library/system/io): use type classes 2017-03-23 14:29:07 -07:00
Gabriel Ebner
c8fff9f4ff refactor(init/meta/interaction_monad): replace rstep by istep 2017-03-23 09:03:41 +01:00
Leonardo de Moura
6887a99f08 feat(library/init/category/state): make state and state_t universe polymorphic 
The new definitions are not fully general since they force data and
state to be in the same universe.
 2017-03-22 23:45:29 -07:00
Leonardo de Moura
60dd85719c feat(library/system/io): system.io without axioms 2017-03-22 23:36:05 -07:00
Sebastian Ullrich
897b4f9db1 fix(frontends/lean/builtin_exprs): override scope behavior for strict quoted names 2017-03-22 07:34:50 -07:00
Sebastian Ullrich
793f0baee8 feat(library/tactic/vm_monitor): use attribute for registering VM monitors 2017-03-22 07:34:27 -07:00
Leonardo de Moura
a31de3b7bc feat(library/unification_hint): improve unification_hint matcher 
Improvements:
- Use heuristic match explicit arguments first and then match implicit.
- Skip annotations.
- Follow metavariable assigments.
- Use is_def_eq when pattern doest not contain matching variables.
 2017-03-21 10:19:34 -07:00
Leonardo de Moura
aa68d72fa5 fix(library/equations_compiler/elim_match): skip nonvar + inaccessible 2017-03-21 08:08:36 -07:00
Leonardo de Moura
fdadada3a9 fix(frontends/lean): fixes #1468 
@kha I had to add yet another hack to fix this issue.

In notation declarations, names are resolved at notation declaration time.
So, users do not expect them to be resolved again at tactic execution time.

I addressed this problem by wrapping constants occurring in notation
declarations with a "frozen_name" annotation. This transformation is
only performed if m_in_quote is true.
Then resolve_names_fn at elaborator.cpp will not try to resolve the
names again.

This change broke two other modules. `-` notation for inverting
equations at `rw`, and `calc` expressions inside quotes.
The broke for the same reason. They were not expecting the constants
to be wrapped with an annotation.
 2017-03-18 13:48:21 -07:00
Sebastian Ullrich
421a6d6f01 feat(frontends/lean/interactive,emacs): highlight current tactic parameter 2017-03-17 18:20:44 -07:00
Leonardo de Moura
11dcab1b31 fix(frontends/lean/elaborator): fixes #1458 2017-03-16 10:31:21 -07:00
Daniel Selsam
cddf5f081d fix(library/tactic/kabstract.cpp): only use replace_fn cache if replacing all occs 2017-03-15 19:40:52 -07:00
Daniel Selsam
9135e231f0 fix(tests/lean/inductive_sorry.lean): fix broken test 2017-03-15 19:40:52 -07:00
Leonardo de Moura
83fbb605f4 chore(tests/lean): fix tests 2017-03-15 19:40:52 -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
647d7a8501 fix(frontends/lean/elaborator): expr patterns should ignore binding names 2017-03-15 14:06:00 -07:00
Leonardo de Moura
8d409d7c63 feat(library/unification_hint): unification hint validation 2017-03-12 16:42:16 -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
740d42ea45 fix(library/tactic): we should preserve names when using the revert/do_something/intro idiom 2017-03-11 12:20:39 -08:00
Daniel Selsam
538ac8d187 feat(inductive_compiler): generate injectivity lemmas 2017-03-10 22:27:18 -08:00
Sebastian Ullrich
16558bf082 refactor(library,library): rename pre_monad to has_bind 2017-03-09 20:32:25 -08:00
Sebastian Ullrich
763097dbd2 refactor(library): revise the monadic hierarchy 2017-03-09 20:30:03 -08:00
Leonardo de Moura
b0a33259ee fix(library/compiler/simp_inductive): array^.data should not be treated as a regular projection 2017-03-09 19:11:51 -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
e875141322 feat(library/tactic/intro_tactic): make sure unused names are used if the user did not provide them 2017-03-09 16:03:18 -08:00
Leonardo de Moura
8979663164 feat(library/tactic/simplify): relax reducibility constraints when matching implicit arguments 
Motivation: if the explicit part matches (what the user sees), then the implicit part must morally match too.
If it doesn't because of reducibility setting, the behavior is usually counterintuitive.
 2017-03-08 20:08:54 -08:00
Leonardo de Moura
4ab0a6d8d2 fix(library): problems with the subtype constructor and field renaming 
The problem was not detected by the test suite because of issue #1446
 2017-03-08 19:42:12 -08:00
Jeremy Avigad
666ca36470 fix(library/tests/lean/*): fix tests 2017-03-08 19:31:27 -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
Leonardo de Moura
7a99d87cbd fix(library/tactic/ac_tactics): allow nested ac_app macros in perm_ac macro 
fixes #1442
 2017-03-08 13:46:49 -08:00
Daniel Selsam
42e08cac36 chore(tests/lean/run/1430.lean): repro for #1430 2017-03-07 20:12:07 -08:00
Leonardo de Moura
1ac240e2db chore(tests/lean): fix tests 2017-03-07 19:45:00 -08:00