Leonardo de Moura
3c71d7eda2
feat(frontends/lean,library/tactic/tactic_state): improve error localization
2016-09-25 18:40:41 -07:00
Leonardo de Moura
bbf21b4e65
feat(frontends/lean/begin_end_block): auto-quote identifiers
2016-09-25 17:25:21 -07:00
Leonardo de Moura
8b132c758a
feat(frontends/lean/begin_end_block): add basic auto-quotation
2016-09-25 17:03:12 -07:00
Leonardo de Moura
97261fcc48
feat(frontends/lean): add very basic 'begin ... end' block support
2016-09-24 21:27:27 -07:00
Leonardo de Moura
5957022adb
feat(frontends/lean): add 'class' keyword
2016-09-24 14:32:01 -07:00
Leonardo de Moura
03e4fd1038
feat(frontends/lean,library): cleanup instance cmd, and use 'meta instance'
2016-09-24 12:33:25 -07:00
Leonardo de Moura
148da46481
feat(frontends/lean): 'mutual' and 'meta' are now keywords
2016-09-24 10:44:40 -07:00
Leonardo de Moura
9991d61610
chore(library/init): cleanup
2016-09-23 14:53:17 -07:00
Gabriel Ebner
3ef9149902
feat(library/tactic/tactic_state): add get_unused_name
2016-09-19 16:38:03 -07:00
Leonardo de Moura
24f1cb2726
chore(frontends/lean): new_elaborator is now the default
2016-09-19 16:34:06 -07:00
Leonardo de Moura
90bfd84a07
feat(frontends/lean): Type is now (Type 1)
...
In the standard library, we should use explicit universe variables for
universe polymorphic definitions.
Users that want to declare universe polymorphic definitions but do not
want to provide universe level parameters should use
Type _
or
Type*
2016-09-17 14:30:54 -07:00
Leonardo de Moura
7b1811ccd6
refactor(library/init): move more files to new elaborator
2016-09-15 14:58:52 -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
39dc336310
feat(library/tactic/user_attribute): add set_basic_attribute and unset_attribute tactics
2016-09-01 14:17:05 -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
Jeremy Avigad
766f3f18ee
feat(library/init/meta/tactic): generalize first for any return type
2016-08-21 22:31:54 -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
cd77f7167e
chore(frontends/lean): run_tactic ==> run_command
...
add `command` as alias for `tactic unit`
2016-08-18 12:53:21 -07:00
Leonardo de Moura
ddc3789929
feat(frontends/lean): add run_tactic command
...
This commit also adds the tactic `add_decl`.
2016-08-18 10:56:18 -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
Leonardo de Moura
c9475774f4
feat(library/tactic/tactic_state): add is_def_eq and is_def_eq_core tactics
2016-08-16 11:08:03 -07:00
Leonardo de Moura
f8e5753a13
feat(library/type_context, library/tactic): add eta-expansion method and tactic
2016-08-14 16:15:12 -07:00
Leonardo de Moura
2354b63099
feat(library/tactic/tactic_state): add whnf_core
2016-08-14 16:02:40 -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
7bb6ccc089
refactor(library/init/meta): qexpr ==> pexpr
2016-08-05 17:04:36 -07:00
Leonardo de Moura
38b81f2656
refactor(library/init/meta): remove base_tactic
...
We don't need it.
2016-08-04 19:17:08 -07:00
Leonardo de Moura
c1793cd620
feat(library/init/meta/tactic): add 'refine' tactic
2016-07-31 21:17:19 -07:00
Leonardo de Moura
6d0fa806d8
feat(library/tactic/elaborate): convert unassigned metavars into new goals
2016-07-31 20:38:57 -07:00
Leonardo de Moura
12fa52c77d
feat(library/tactic, frontends/lean/elaborator): add to_expr tactic
2016-07-31 20:21:17 -07:00
Sebastian Ullrich
e090326f98
fix(library): remove classical instances from global scope
2016-07-29 23:44:23 -04:00
Leonardo de Moura
7ddf1e817b
chore(frontends/lean): coercions are disabled by default
2016-07-29 13:03:23 -07:00
Leonardo de Moura
0db1f3a9d1
feat(library/init/meta): add helper functions
2016-07-23 11:39:11 -07:00
Leonardo de Moura
212d222047
feat(frontends/lean): quoted names
2016-07-22 19:06:57 -07:00
Leonardo de Moura
fa04e5f36f
refactor(library/init/meta): move set/get option tactics to separate file
2016-07-21 17:10:38 -07:00
Leonardo de Moura
ada260309e
refactor(library/init/meta): move defeq simplifier related tactics to separate file
2016-07-21 17:07:09 -07:00
Leonardo de Moura
d70bf2f04e
refactor(library/init/meta): move simplifier related tactics to separate file
2016-07-21 17:03:19 -07:00
Leonardo de Moura
1b55507971
refactor(library/init/meta): rename C++ intro to intro_core, and define smarter intro in C++
2016-07-21 16:54:23 -07:00
Leonardo de Moura
2580b40dc1
feat(library/init/meta/tactic): add helper tactic whnf_target
2016-07-20 19:29:22 -04:00
Leonardo de Moura
7f0276f592
feat(library/tactic): add 'rewrite' tactic and variants
2016-07-17 16:08:11 -04:00
Leonardo de Moura
26177995c2
feat(library/tactic): add 'generalize' tactic
2016-07-16 15:41:32 -04:00
Leonardo de Moura
a5307a34bc
feat(library/tactic): add 'cases' tactic skeleton
2016-07-12 14:05:03 -04:00
Leonardo de Moura
e48fa15b71
feat(library/tactic/backward/backward_chaining): add 'pre_tactic' to backward_chaining_core
2016-07-10 16:11:13 -07:00
Leonardo de Moura
7c8d0f444f
feat(library/tactic/backward): finish backward chaining tactic
2016-07-10 13:49:28 -07:00
Leonardo de Moura
af9c7148b3
feat(library/tactic/backward): add backward_chaining skeleton tactic
2016-07-10 11:45:25 -07:00
Leonardo de Moura
aacd812cc8
feat(library/init/meta/tactic): add 'by_contradiction' tactic
2016-07-09 19:14:36 -07:00
Leonardo de Moura
f81daab596
feat(library/init): add 'has_andthen' type class, and ';' notation
2016-07-09 18:39:27 -07:00
Leonardo de Moura
6b30b89c89
feat(library/init/meta/tactic): add 'simp_at' tactics
2016-07-09 17:23:45 -07:00
