Leonardo de Moura
b5e0ded163
feat(frontends/lean): max precedence used by Lean is not max_uint anymore
...
The motivation is to allow users to define notation with higher
precedence than function application.
2014-11-07 07:57:11 -08:00
Leonardo de Moura
85d0521d48
feat(frontends/lean): add '[parsing-only]' modifier to notation declarations, closes #305
2014-11-06 21:34:05 -08:00
Leonardo de Moura
8d05238533
fix(kernel/error_msgs): ignore binder information when comparing type mismatches, fixes #304
2014-11-06 21:03:51 -08:00
Leonardo de Moura
ed83b7ff2a
fix(emacs/lean-syntax): syntax highlight, issue #306
...
1- FIXED structure foo := (bar : Type) -- the name of structures is not highlighted
2- NOT FIXED check foo-- this comment is not highlighted
3- FIXED check Type.{5} -- Type is not highlighted
4- FIXED definition bar{thisishighlighted : Type} := foo
5- FIXED definition bar2 {thetypeofthisvariableisnothighlighted :Type} := foo
Have no idea what is going on with 2. I'm not sure if this is our bug,
or Emacs code we depend on.
2014-11-06 20:59:31 -08:00
Leonardo de Moura
af88e34588
fix(kernel/inductive): bug in eliminator for recursive datatypes in Prop
2014-11-06 14:03:28 -08:00
Leonardo de Moura
be52d950f0
fix(frontends/lean): improve error message, addresses issue #299
2014-11-06 12:19:40 -08:00
Leonardo de Moura
e499f8e20a
feat(kernel/inductive): relax conditions for an inductive datatype in Prop to be able to eliminate into Type
...
The new relaxed version allows us to define the "accessability"
proposition and have an eliminator into Type.
See justification in the new comments at inductive.cpp
2014-11-06 09:36:54 -08:00
Leonardo de Moura
8723f5b613
fix(frontends/lean/inductive_cmd): inductive datatype elaborator was 'fixing' parameter mismatches.
...
Given a datatype C with parameters As, if the declaration contained
(C Bs), the elaborator would silently replace it with (C As).
This bug would confuse users and make them believe they define something
different.
2014-11-05 23:12:00 -08:00
Leonardo de Moura
b3ad8c704a
feat(frontends/lean/structure_cmd): allow inheritance from two identical structures, closes #296
2014-11-05 15:01:05 -08:00
Leonardo de Moura
4650791108
feat(frontends/lean): add 'print fields' command
2014-11-05 14:06:54 -08:00
Leonardo de Moura
677e0aeef6
fix(frontends/lean/structure_cmd): accept ': Type' when universe levels are not specified
2014-11-05 12:02:52 -08:00
Leonardo de Moura
d6dc624ca8
fix(frontends/lean/structure_cmd): error parsing structure without parameters followed by ': Type'
2014-11-05 12:02:52 -08:00
Leonardo de Moura
defc2478b5
feat(frontends/lean): add 'record' as an alias for 'structure' command
2014-11-05 12:02:52 -08:00
Soonho Kong
e71db7109d
fix(emacs/lean-mode.el): remove quotation marks in lean-execute
...
Close #294
2014-11-05 09:20:14 -05:00
Leonardo de Moura
5b87d060cf
fix(frontends/lean/structure_cmd): universe level validation
2014-11-04 22:19:23 -08:00
Leonardo de Moura
6944c7d902
fix(frontends/lean/placeholder_elaborator): local context must be adjusted when performing class-instance resolution modulo Pi-abstraction, fixes #293
2014-11-04 18:41:27 -08:00
Leonardo de Moura
b5ad0fb504
refactor(frontends/lean/local_context): add 'const' modifier
2014-11-04 18:37:31 -08:00
Leonardo de Moura
3bfe5b0b7e
fix(frontends/lean): type information for "atomic" notation declaration, fixes #292
2014-11-04 18:01:20 -08:00
Leonardo de Moura
fa405d7884
refactor(frontends/lean): combine info annotations in a single module
2014-11-04 18:01:20 -08:00
Leonardo de Moura
c6c090eda6
feat(src/emacs/lean-mode): add shortcut for restarting lean server
2014-11-04 18:01:20 -08:00
Soonho Kong
2273f75e9b
fix(emacs/lean-mode): handle when there is spaces in filenames
2014-11-04 19:22:35 -05:00
Soonho Kong
53e18d0e39
chore(src/CMakeLists.txt): copy linja and ltag to bin when install
2014-11-04 18:16:04 -05:00
Leonardo de Moura
60eac0195d
feat(frontends/lean/structure_cmd): generate projection over constructor theorems for structures
2014-11-04 09:10:25 -08:00
Leonardo de Moura
d58c3e498d
feat(frontends/lean/builtin_cmds): add 'print prefix' command
2014-11-04 08:40:32 -08:00
Leonardo de Moura
3454e70017
fix(frontends/lean/inductive_cmd): bug in expression position propagation, fixes #289
...
Fix incorrect line/column number information in error messages produced
during inductive datatype elaboration.
2014-11-04 07:44:47 -08:00
Leonardo de Moura
b6722a5d33
feat(frontends/lean/structure_cmd): add 'private' modifier for parent structures
...
When it is used coercions/instances to parent structure are to registered
2014-11-03 23:16:49 -08:00
Leonardo de Moura
b24165dc7b
feat(frontends/lean/structure_cmd): remove 'cases_on' for structures since it may confuse users, add 'destruct' as alternative name for 'rec_on'
2014-11-03 23:06:33 -08:00
Leonardo de Moura
7897e21a14
feat(frontends/lean/structure_cmd): allow fields to be suppresed, but constructor to be provided
2014-11-03 22:55:51 -08:00
Leonardo de Moura
08b4ce2db9
feat(frontends/lean/structure_cmd): use 'mk' as constructor name when it is not provided
2014-11-03 22:40:08 -08:00
Leonardo de Moura
8f3139231b
feat(frontends/lean/structure_cmd): allow structure declarations that contains only a header
2014-11-03 22:17:43 -08:00
Leonardo de Moura
91749d2364
fix(frontends/lean/structure_cmd): modify coercion generation
...
The previous coercion was more efficient, but the computation was
getting stuck when processing algebraic structures
2014-11-03 19:37:11 -08:00
Leonardo de Moura
edd94c00df
fix(library/definitional): add missing files
2014-11-03 18:36:25 -08:00
Leonardo de Moura
c306bfa83c
feat(frontends/lean/structure_cmd): add 'eta' theorem for structures
2014-11-03 18:33:44 -08:00
Leonardo de Moura
101e9966fd
fix(emacs/lean-syntax): bug in syntax highlight, examples do not have names
2014-11-03 18:32:18 -08:00
Leonardo de Moura
186d910d0b
feat(frontends/lean/structure_cmd): mark coercion to parents as coercions and instances (when both structures as classes)
2014-11-03 17:55:59 -08:00
Leonardo de Moura
9531203d9d
feat(frontends/lean/structure_cmd): mark structure as 'class' when [class] modifier is used
2014-11-03 17:47:08 -08:00
Leonardo de Moura
b112f3c582
feat(frontends/lean/structure_cmd): add coercions to parent structures
2014-11-03 17:39:52 -08:00
Leonardo de Moura
922e66c42f
fix(frontends/lean/decl_cmds): do not save 'examples' in .ilean file
2014-11-03 16:13:46 -08:00
Leonardo de Moura
7afa69577e
feat(frontends/lean/structure_cmd): add aliases for structure decls
2014-11-03 15:50:41 -08:00
Leonardo de Moura
efe1105eb9
fix(frontends/lean): alias generation for composite names was not working
...
This is an issue for declarations that generate composite names such as
the inductive datatype packacke.
The commit also fix a bug in the generate of aliases for recursors
2014-11-03 15:43:58 -08:00
Leonardo de Moura
594e3ea8fc
fix(frontends/lean/structure_cmd): 'rec' must be marked as protected
2014-11-03 14:50:12 -08:00
Leonardo de Moura
5872c93eaf
feat(frontends/lean/structure_cmd): add structure_cmd core
2014-11-03 14:14:40 -08:00
Leonardo de Moura
a2e75159c8
fix(frontends/lean): process choice-exprs at check_constant_next
2014-11-02 19:42:30 -08:00
Leonardo de Moura
c7406d6ce8
fix(library/scoped_ext): bug when declaring nested namespaces
2014-11-02 15:35:49 -08:00
Leonardo de Moura
df008dc3c3
feat(frontends/lean/inductive_cmd): create a namespace for each declared datatype
2014-11-01 19:15:46 -07:00
Leonardo de Moura
ea55ec4090
feat(frontends/lean/decl_cmds): remove useless name from 'example' commad
2014-11-01 16:12:23 -07:00
Leonardo de Moura
1e6f7cdbb4
chore(frontends/lean/decl_cmds): add 'example' command
...
It is like a theorem, but it is discarded after checking
2014-11-01 11:37:39 -07:00
Leonardo de Moura
b1c2efecbb
chore(frontends/lean/decl_cmds): add missing static
2014-11-01 11:18:10 -07:00
Leonardo de Moura
94cf10284a
fix(frontends/lean/calc_proof_elaborator): bug when inserting symmetry proofs for heq, fixes #286
...
The problem was that heq type is
Pi {A : Type} (a : A) {B : Type} (b : B), Prop
The calc_proof_elaborator was assuming that (a : A) (b : B) were the
last two arguments in any relation supported by calc.
The fix is to remove this assumption.
2014-11-01 07:30:04 -07:00
Leonardo de Moura
2688ca38bf
feat(frontends/lean/inductive_cmd): notation for enumeration types
2014-10-31 19:01:32 -07:00
