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
Leonardo de Moura
bb6945d384
chore: update stage0
2020-11-20 12:37:12 -08:00
Leonardo de Moura
72032980ff
feat: support for unboundImplicitLocals at variable and variables commands
...
They are morally part of the header.
cc @Kha
2020-11-20 12:32:32 -08:00
Leonardo de Moura
f3779f1542
feat: add support for unbound implicit locals
2020-11-20 12:22:27 -08:00
Leonardo de Moura
5adfd37dfd
feat: add auxiliary KVMap for storing extra information at Exception.internal
2020-11-20 09:49:00 -08:00
Leonardo de Moura
2a769bbd79
feat: add missing keywords
2020-11-20 09:45:36 -08:00
Sebastian Ullrich
f6943d9c13
doc: fix highlighting of #eval etc.
2020-11-20 16:59:23 +01:00
Sebastian Ullrich
1e2c0d1d41
doc: remove "section" keywords, which aren't highlighted
2020-11-20 16:59:23 +01:00
Sebastian Ullrich
23bedc5ef5
doc: inline un-minified highlightjs-lean code into highlight.js
2020-11-20 16:59:23 +01:00
Leonardo de Moura
40ab77288d
fix: namespaces.md
2020-11-20 07:56:53 -08:00
Leonardo de Moura
eba78e2d83
test: renaming for intrinsically typed lambda calculus
2020-11-19 19:10:49 -08:00
Leonardo de Moura
594c5a52f6
fix: sections.md
2020-11-19 19:06:06 -08:00
Leonardo de Moura
5fe11e0f00
doc: move example to tour.md
2020-11-19 17:38:51 -08:00
Leonardo de Moura
b619f09010
doc: section, variables and namespaces
2020-11-19 17:34:08 -08:00
Leonardo de Moura
3323f7da60
feat: add instance Inhabited (Sort u)
2020-11-19 13:55:00 -08:00
Leonardo de Moura
e29cc367f3
feat: test each example using a separate file
2020-11-19 13:51:52 -08:00
Leonardo de Moura
72a6ce498a
chore: move lean3changes.md
2020-11-19 12:57:41 -08:00
Leonardo de Moura
a1c52ae1c4
doc: expand functions.md
2020-11-19 12:48:51 -08:00
Leonardo de Moura
918420744e
feat: add whatIsLean.md
2020-11-19 11:33:13 -08:00
Leonardo de Moura
90298ba476
feat: add helper instance
2020-11-19 11:32:54 -08:00
