Sebastian Ullrich
0212ccd3e2
feat: Nix: compatibility default.nix
2020-11-24 19:16:27 +01:00
Sebastian Ullrich
c6929ae69a
feat: Nix: basic setup
2020-11-24 19:16:27 +01:00
Sebastian Ullrich
56d6bbbf05
doc: phrasing
2020-11-24 15:58:10 +01:00
Leonardo de Moura
f37fd97d9f
chore: fix test
2020-11-23 18:34:38 -08:00
Leonardo de Moura
a44e51ce2e
fix: identifiers highlighting and literals
2020-11-23 18:32:39 -08:00
Leonardo de Moura
0fc0bf0593
chore: use instance ... where in the docs
2020-11-23 18:30:21 -08:00
Leonardo de Moura
f456e006dc
chore: test instance ... where
2020-11-23 18:24:23 -08:00
Leonardo de Moura
0a3d584ef2
chore: update stage0
2020-11-23 18:09:10 -08:00
Leonardo de Moura
5884b9c19a
feat: add support for instance ... where
...
@Kha The fields are not mutually recursive yet, but it is good enough
for writing examples in the manual.
See new test
2020-11-23 18:07:02 -08:00
Leonardo de Moura
645c1034a0
chore: reduce compilation time
2020-11-23 16:18:55 -08:00
Leonardo de Moura
be812081f4
chore: using "unbound implicit locals"
2020-11-23 13:09:02 -08:00
Leonardo de Moura
cc321a9d75
chore: update stage0
2020-11-23 12:09:37 -08:00
Leonardo de Moura
ac85650e0a
feat: add optional where clause at declarations
...
closes #191
@Kha Note that it expands into a "let rec".
There are many other places where an optional `where`-clause is
useful. We can add them later. It is relatively easy to add support in
other places using the new helper functions
`expandWhereDeclsOpt` and `expandMatchAltsWhereDecls`
2020-11-23 12:04:51 -08:00
Leonardo de Moura
74c604e51e
chore: update stage0
2020-11-23 10:50:31 -08:00
Leonardo de Moura
3f27d7318e
chore: prepare to add where clause to declarations
2020-11-23 10:41:12 -08:00
Leonardo de Moura
3d68a59366
chore: add link to manual
2020-11-23 10:21:52 -08:00
Leonardo de Moura
5b23efc112
chore: update FAQ
2020-11-23 10:19:15 -08:00
Leonardo de Moura
d5c7f91b83
chore: reorg manual main page
2020-11-23 09:58:51 -08:00
Leonardo de Moura
f7279ee419
test: add tests for some Lean3 issues
2020-11-23 09:55:39 -08:00
Leonardo de Moura
b4012fdd71
chore: remove old comment that is not true anymore
2020-11-23 08:44:50 -08:00
Leonardo de Moura
a297d4107e
doc: add tactics.md
2020-11-22 21:15:55 -08:00
Leonardo de Moura
9608ea5aef
doc: do notation
2020-11-22 16:15:33 -08:00
Leonardo de Moura
cb9574b086
chore: test unboundImplicitLocals and cleanup
2020-11-22 10:33:28 -08:00
Leonardo de Moura
e76a0d0b25
chore: update stage0
2020-11-22 10:17:49 -08:00
Leonardo de Moura
da3e3211a0
feat: refine propagateExpectedType
2020-11-22 10:16:41 -08:00
Leonardo de Moura
29303f17f3
chore: test unboundImplicitLocals
2020-11-22 09:48:15 -08:00
Leonardo de Moura
8e15159973
chore: update stage0
2020-11-22 09:33:53 -08:00
Leonardo de Moura
8ed3b8c55f
fix: tryPureCoe?
2020-11-22 08:24:56 -08:00
Leonardo de Moura
e8ae23b7a6
chore: minor
2020-11-21 20:53:19 -08:00
Leonardo de Moura
8598dde6e6
fix: if-then-else elaboration issue
...
@Kha I hate this kind of hack, but the behavior looked unacceptabled
to me. I added a big comment describing the issue and the hack.
2020-11-21 20:51:28 -08:00
Leonardo de Moura
7496f4377f
fix: issues with unbound implicit locals
...
This commit also add support for them in the `inductive` command.
2020-11-21 16:17:38 -08:00
Leonardo de Moura
b415648fff
chore: update stage0
2020-11-21 14:45:47 -08:00
Leonardo de Moura
f220654a27
feat: default instances
2020-11-21 14:44:40 -08:00
Leonardo de Moura
6a4e4c7127
chore: update stage0
2020-11-21 11:15:36 -08:00
Leonardo de Moura
c7a31ed52e
chore: remove duplicate instances
2020-11-21 11:05:52 -08:00
Leonardo de Moura
050bdd2e88
feat: readable auto generated instance names
2020-11-21 11:05:28 -08:00
Leonardo de Moura
3ff494832d
chore: cleanup
2020-11-21 08:59:21 -08:00
Leonardo de Moura
b672e37bcc
chore: annotate OfNat and ToString default instances
2020-11-21 08:34:45 -08:00
Leonardo de Moura
84741279c0
chore: update stage0
2020-11-21 08:27:23 -08:00
Leonardo de Moura
76025c9d18
feat: add attribute [defaultInstance]
2020-11-21 08:24:28 -08:00
Leonardo de Moura
fa6d35adfa
chore: fix tests
2020-11-20 17:00:13 -08:00
Leonardo de Moura
8dfb0324c5
chore: update stage0
2020-11-20 16:53:19 -08:00
Leonardo de Moura
6830291fd5
chore: remove dead code at Class.lean used by old frontend
2020-11-20 16:51:44 -08:00
Leonardo de Moura
104ade010f
chore: weird line break
2020-11-20 16:22:01 -08:00
Leonardo de Moura
e6215f7282
chore: remove some unnecessary commas
2020-11-20 15:47:27 -08:00
Leonardo de Moura
c9cbe35916
fix: adjust code to optional , at structure instances
...
@Kha I implemented the optional `,` at structure instances.
You have suggested it a few weeks/months ago. F# also implements this
feature. I got back to it while write documentation for Lean.
It looks quite nice when we are packing many functions into a structure.
BTW, F# also has optional separators for list literals :)
This is a much simpler change for us since `[...]` is defined using
the `syntax/macro_rules` commands, but I didn't find optional ','
would very useful since our list literals are usually in a single
line.
2020-11-20 15:43:35 -08:00
Leonardo de Moura
ec19dab171
chore: update stage0
2020-11-20 15:25:25 -08:00
Leonardo de Moura
fcbd72f2af
feat: optional , at structure instances
2020-11-20 15:24:34 -08:00
Leonardo de Moura
8d032abcd5
chore: update stage0
2020-11-20 14:01:12 -08:00
Leonardo de Moura
27e26998d2
chore: prepare to change structInst syntax
2020-11-20 13:57:52 -08:00
