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

1685 commits

Author SHA1 Message Date
Leonardo de Moura
0d97700c60 feat(library/compiler): add support for and.rec in the code generator 2017-04-16 13:31:37 -07:00
Sebastian Ullrich
26ac6d31f2 fix(library/metavar_util): do not compress mvar assignments in tmp mode 2017-04-16 09:35:49 -07:00
Gabriel Ebner
cefc26d9cb refactor(library/system/process): add exit status and working directory 2017-04-11 16:42:17 -07:00
Gabriel Ebner
c06bef0505 fix(library/aux_definition): also zeta expand the local context 
@leodemoura The forced zeta-expansion in mk_aux_definition might
cause problems if we use tactic.abstract without zeta-reduction.
However, we never use the non-zeta mode, and it already fails right now
if you accidentally use zeta-expansion in the proof we want to abstract.
 2017-04-04 09:04:37 +02:00
Sebastian Ullrich
669c4130b1 fix(frontends/lean/builtin_expr): no field notation after @/@@ 2017-03-31 09:40:49 -07:00
Sebastian Ullrich
4a33045b84 chore(tests/lean,shell/lean): run leantests and leanruntests in parallel 2017-03-30 06:04:00 +02:00
Leonardo de Moura
ad859817b1 feat(frontends/lean): allow local decls to shadow namespaces 2017-03-29 16:09:45 -07:00
Jared Roesch
dc4086d0ed feat(library/vm/process): add basic process support 2017-03-28 18:08:06 -07:00
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