Leonardo de Moura
148da46481
feat(frontends/lean): 'mutual' and 'meta' are now keywords
2016-09-24 10:44:40 -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
001e06abdc
chore(library/init): use 'instance'
2016-09-23 14:00:34 -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
015c667eae
fix(tests/lean/run/IO2): bad overload
2016-09-23 09:34:19 -07:00
Leonardo de Moura
b55a17614a
feat(frontends/lean): structure instances
2016-09-21 22:52:43 -07:00
Leonardo de Moura
952974f024
test(tests/lean/run/pred_to_subtype_coercion): add coercion to subtype test
2016-09-21 17:10:56 -07:00
Leonardo de Moura
b7abd61579
feat(frontends/lean): change subtype notation (again)
...
We had conflicts with the set notation.
2016-09-21 17:02:18 -07:00
Leonardo de Moura
973bc5f1d6
feat(frontends/lean): add notation for 'sep'
2016-09-21 16:29:59 -07:00
Leonardo de Moura
c0ff9967af
feat(frontends/lean): add basic notation for collections
2016-09-21 16:20:57 -07:00
Leonardo de Moura
5e5285ee67
refactor(library): rename pr1/pr2 ==> fst/snd
2016-09-21 09:48:39 -07:00
Leonardo de Moura
9df712581b
chore(frontends/lean): remove 'new_elaborator' option
2016-09-20 08:32:37 -07:00
Leonardo de Moura
9f1a576e98
chore(frontends/lean): remove dead code from parser
2016-09-19 17:04:59 -07:00
Leonardo de Moura
325177bfd9
chore(tests/lean): make sure all tests can be processed using new elaborator
2016-09-19 16:17:32 -07:00
Leonardo de Moura
bc5504b482
fix(tests/lean/run): disable tests that do not type check in the elaborator because it doesn't unfold theorems
2016-09-19 15:34:12 -07:00
Leonardo de Moura
b0361b49e2
chore(tests/lean/run/662): move test to new elaborator
2016-09-19 14:36:46 -07:00
Leonardo de Moura
1cf5419757
chore(tests/lean/run): move tests to new elaborator
2016-09-19 11:43:59 -07:00
Leonardo de Moura
e4553e0446
fix(library/type_context): bug in occurs check
2016-09-19 11:40:00 -07:00
Leonardo de Moura
10f4a22fff
fix(frontends/lean/elaborator): try to synthesize pending type class instances before processing eliminator/recursor
2016-09-19 11:14:49 -07:00
Leonardo de Moura
fab357dd94
chore(tests/lean/run): move tests to new elaborator
2016-09-19 11:04:14 -07:00
Leonardo de Moura
6bfecdf00c
chore(tests/lean/run): move tests to new elaborator
2016-09-18 19:10:48 -07:00
Leonardo de Moura
677d3d4cf9
fix(frontends/lean/elaborator): ignore annotations around function when deciding which kind of elaborator strategy should be used
2016-09-18 19:10:13 -07:00
Leonardo de Moura
c81f283068
chore(tests/lean/run): move tests to new elaborator
2016-09-18 18:38:41 -07:00
Leonardo de Moura
4e0e812811
fix(frontends/lean/builtin_exprs): patterns in do-notation
2016-09-18 18:19:51 -07:00
Leonardo de Moura
bc31e43317
chore(tests/lean/run): delete old tests
2016-09-18 18:19:04 -07:00
Leonardo de Moura
ba974cc1d6
refactor(library/init/state): fix stateT at universe 1
2016-09-18 17:48:37 -07:00
Leonardo de Moura
5df705ebe8
fix(library/equations_compiler/compiler): nested match-exprs in meta_definitions
2016-09-18 17:20:52 -07:00
Leonardo de Moura
98da86eac0
chore(tests/lean/run): move tests to new elaborator
2016-09-18 17:13:13 -07:00
Leonardo de Moura
51845d1622
fix(frontends/lean/parser): support as_atomic exprs at to_pattern_fn
2016-09-18 16:55:59 -07:00
Leonardo de Moura
194d1be0dd
fix(library/equations_compiler/structural_rec): reflexive type support
2016-09-18 16:15:31 -07:00
Leonardo de Moura
06df5fef1d
chore(tests/lean/run): make sure tests work with new elaborator
2016-09-18 14:48:47 -07:00
Leonardo de Moura
6657876566
feat(library/equations_compiler): add support for meta_definitions
2016-09-18 10:52:38 -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
928d567a3f
chore(tests/lean): providing universes
2016-09-17 12:54:20 -07:00
Leonardo de Moura
f8df2cd44f
fix(frontends/lean/decl_util): section variables/parameters
2016-09-16 15:32:51 -07:00
Daniel Selsam
52f87760d8
feat(src/library/inductive_compiler): support for nested inductive types
2016-09-16 12:50:59 -07:00
Leonardo de Moura
f60de96d98
fix(frontends/lean/elaborator): bug at @@ annotation
2016-09-15 17:03:59 -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
6c84a0a7b1
feat(frontends/lean): use new notation for declaring universes in constant and structure decls
2016-09-13 21:45:16 -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
cf1c50f4e9
fix(frontends/lean/elaborator): get_elim_info_for_builtin
2016-09-13 14:17:08 -07:00
Leonardo de Moura
9765151156
feat(kernel/inductive): relax restriction on metavariables
...
This change does not affect correctness of the kernel, since QED only
process terms that do not contain metavariables.
2016-09-13 13:50:04 -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
9632f00fbe
test(tests/lean/run): the lean2 macro dec_trivial is tricky to support in the new elaborator
...
Here are some workarounds.
2016-09-13 08:09:12 -07:00
Leonardo de Moura
cf30d31024
fix(library/tactic/cases_tactic): missing case
2016-09-12 17:41:22 -07:00
Leonardo de Moura
0b90ace9f8
feat(frontends/lean/builtin_exprs): basic support for let-expr with patterns
2016-09-11 22:21:10 -07:00
Leonardo de Moura
b957d3ee94
fix(frontends/lean/parser): make sure anonymous constructors can be used in patterns
2016-09-11 22:13:50 -07:00
Leonardo de Moura
38f7f9bbdc
fix(library/type_context): ignore unification constraints of the form ?m =?= delayed[?m]
2016-09-11 17:25:30 -07:00
Leonardo de Moura
24f76d5260
feat(frontends/lean/elaborator): improve convoy and elim
2016-09-10 22:51:26 -07:00
Leonardo de Moura
214e91d1ae
feat(frontends/lean/elaborator): improve match_convoy in the new elaborator
2016-09-10 21:41:40 -07:00
