Leonardo de Moura
4500c3ecfe
feat(library/init/logic): lemmas for rewriting let-exprs
2016-10-15 17:23:18 -07:00
Leonardo de Moura
476684a284
refactor(library,library/tactic/defeq_simplifier): use simp_lemmas in the defeq_simplifier
2016-10-08 22:15:27 -07:00
Leonardo de Moura
96538ba899
refactor(library/init): add basic order classes
2016-10-02 07:53:37 -07:00
Leonardo de Moura
978f1d1bea
feat(library/init/logic): add universe lifting operation
2016-09-28 11:37:05 -07:00
Leonardo de Moura
d5a28f91cc
refactor(library/init): reorganize files and cleanup notation
2016-09-25 13:37:45 -07:00
Leonardo de Moura
d944d78b1d
feat(frontends/lean/decl_cmds): attribute list must occur immediately after 'attribute' keyword
2016-09-24 18:40:57 -07:00
Leonardo de Moura
e304d778a1
chore(library/init): cleanup
2016-09-24 16:38:39 -07:00
Leonardo de Moura
49cffc0b20
feat(frontends/lean): add compact notation for setting attributes suggested by Sebastian
2016-09-24 15:45:06 -07:00
Leonardo de Moura
d1653abe57
chore(library/init/logic): cleanup
2016-09-24 14:52:18 -07:00
Leonardo de Moura
5957022adb
feat(frontends/lean): add 'class' keyword
2016-09-24 14:32:01 -07:00
Leonardo de Moura
0641f3f714
chore(library/init): cleanup proofs using new elaborator
2016-09-23 17:36:32 -07:00
Leonardo de Moura
f00e6c0a96
feat(frontends/lean): anonymous instances
...
The instance name is synthesized automatically.
2016-09-23 13:34:34 -07:00
Leonardo de Moura
6bfd4eb9cf
feat(frontends/lean): add 'instance' keyword
2016-09-23 12:19:05 -07:00
Leonardo de Moura
7ae778e925
feat(frontends/lean): generalize '~>' notation, and add alias '^.' for '~>'
2016-09-23 08:18:19 -07:00
Leonardo de Moura
2b570e1eae
refactor(frontends/lean): remove old attributes
2016-09-21 14:22:17 -07:00
Leonardo de Moura
b716827206
chore(library/init): uniform style
2016-09-21 09:21:37 -07:00
Leonardo de Moura
8f2c428800
chore(library/init/logic): enforce style
2016-09-21 09:01:24 -07:00
Leonardo de Moura
318ef761d3
feat(frontends/lean): lambda+anonymous_constructor+match notation
2016-09-21 08:49:05 -07:00
Leonardo de Moura
9df712581b
chore(frontends/lean): remove 'new_elaborator' option
2016-09-20 08:32:37 -07:00
Leonardo de Moura
564bcaab94
chore(library/init): cleanup using anonymous constructor
2016-09-19 10:31:43 -07:00
Leonardo de Moura
382928f0fa
fix(library/init/logic): typo
2016-09-18 10:05:55 -07:00
Leonardo de Moura
5e8f2add84
refactor(library/init): use universe variables
2016-09-17 12:25:02 -07:00
Leonardo de Moura
f42afe2b65
feat(frontends/lean/elaborator): [elab_with_expected_type] is the new default strategy
2016-09-15 14:45:52 -07:00
Leonardo de Moura
688178a2ae
chore(library/init/logic): cleanup proofs
2016-09-15 14:21:41 -07:00
Leonardo de Moura
7f5fe55859
fix(library/init/logic): make sure logic.lean compiles with latest changes
2016-09-15 14:09:12 -07:00
Leonardo de Moura
0871b7734c
chore(library/init/logic): remove leftover
2016-09-14 09:47:35 -07:00
Leonardo de Moura
83cc67ba67
feat(frontends/lean/definition_cmds): use . instead of [none] to represent the empty set of equations
2016-09-14 09:38:30 -07:00
Leonardo de Moura
ce53c035bc
feat(frontends/lean/decl_util): use the same notation for declaring universes in mutual and single decls
2016-09-13 21:05:18 -07:00
Leonardo de Moura
20cce8a0f6
feat(frontends/lean/parser): nicer notation for providing universes
2016-09-13 20:41:00 -07:00
Leonardo de Moura
06de4d156a
refactor(library/init/logic): port to new elaborator
2016-09-13 16:36:09 -07:00
Leonardo de Moura
24049d8f40
refactor(library/init/logic): rename decidable.tt/ff to decidable.is_true/is_false
2016-09-13 13:40:02 -07:00
Leonardo de Moura
d79fbee421
fix(frontends/lean/elaborator): visit_app_with_expected
...
Mark ite and dite with elab_with_expected_type.
2016-09-12 16:48:21 -07:00
Daniel Selsam
b0c5744eea
feat(inductive_compiler): support for mutually inductive types
2016-09-10 14:22:27 -07:00
Leonardo de Moura
91994ff823
feat(frontends/lean/elaborator): switch to new let-decls
2016-09-10 13:00:53 -07:00
Leonardo de Moura
31de40ff4d
refactor(frontends/lean): rename attribute [constructor] ==> [elab_with_expected_type]
2016-09-06 13:12:51 -07:00
Leonardo de Moura
2a912c2650
feat(frontends/lean, library): move constructor attribute to frontend
...
Now, it only affects the elaborator.
2016-09-05 09:34:45 -07:00
Leonardo de Moura
81a30a69d2
refactor(library/normalize): remove unfold and unfold_full attributes
2016-09-05 08:40:58 -07:00
Leonardo de Moura
546f65b542
refactor(init/datatypes, init/logic): define sizeof instances and simp lemmas
2016-09-01 10:33:50 -07:00
Leonardo de Moura
49e368d49e
refactor(library/init): merge datatypes and reserved_notation
2016-09-01 09:50:51 -07:00
Leonardo de Moura
e18500dcd4
feat(frontends/lean/parser): _ is an anonymous variable again in patterns.
2016-08-23 14:06:24 -07:00
Daniel Selsam
4f8db64e23
refactor(simplifier): many fixes, extensions, and tests
...
fix(simplifier): missing simp rule in prop simplifier
fix(library/unfold_macros): do not look for untrusted macros when using sufficient trust level
2016-08-19 14:57:03 -07:00
Leonardo de Moura
e99eb6d47e
feat(frontends/lean): revising inaccessible terms syntax again :(
2016-08-19 13:57:12 -07:00
Leonardo de Moura
93d48ae620
feat(frontends/lean/parser): revised pattern validation
2016-08-17 15:42:13 -07:00
Daniel Selsam
a9b01991c2
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
...
Conflicts:
src/frontends/lean/CMakeLists.txt
src/frontends/lean/structure_cmd.h
2016-08-17 07:34:03 -07:00
Sebastian Ullrich
8bbcbb14cf
chore(library, tests): use new attribute chaining syntax
...
sed -E -i 's/(attribute(\s*(\w|\.)+)* \[[^]]+)\] \[/\1, /' {library,tests}/**/*.lean # repeat as needed
2016-08-16 13:49:03 -07:00
Sebastian Ullrich
fd2c42a8bf
chore(library, tests): switch to new attribute declaration syntax
...
sed -Ei 's/^(\s*)((private |protected )?(noncomputable )?(abbreviation|definition|meta_definition|theorem|lemma|proposition|corollary)\s+\S+\s*)((\s*\[(\S+(\s+[0-9]+)*|priority.*)\])+)\s*/\1attribute \6\n\1\2/' library/**/*.lean tests/**/*.lean
sed -Ei 's/\s+$//' library/**/*.lean # remove trailing whitespace
2016-08-12 15:36:12 -07:00
Sebastian Ullrich
82657b3b64
refactor(library/compiler/inliner, library): replace inline command with attribute
...
sed -Ei 's/inline (protected )?(meta_)?definition (\S+)/\1\2definition \3 [inline]/' library/**/*.lean
2016-08-08 12:45:22 -07:00
Leonardo de Moura
1602a53336
feat(frontends/lean): nary match
2016-08-08 10:04:58 -07:00
Leonardo de Moura
1e6b3614ab
feat(frontends/lean): new pattern matching validation
...
@Kha, we now support variable/constant shadowing in patterns.
A constant may occur in a pattern if it is a constructor or tagged with
the new [pattern] attribute. In the standard library, I have tagged
'add', 'zero', 'one', 'bit0', 'bit1' and 'rfl' with this new attribute.
BTW, arbitrary constants and variables may occur nested in type ascriptions and
inaccessible terms.
Here is an example:
meta_definition tactic_result_to_string {A : Type} : tactic_result A → string
| (success a s) := to_string a
| (exception ⌞A⌟ e s) := "Exception: " ++ to_string (e ())
I had to use the inaccessible ⌞A⌟ in the example above, otherwise, we would be shadowing the parameter
{A : Type}, and we would get a type error.
The new validation is performed at to_pattern_fn (parser.cpp).
2016-08-07 11:31:11 -07:00
Leonardo de Moura
f461b53a7f
refactor(library): remove eq.ops namespace
2016-07-31 12:50:11 -07:00
