2dac93d360
fix: fix noncomputable
...
Also address the changes made to module doc until doc strings are implemented.
2022-02-17 18:59:42 +01:00
d39b14cf7a
chore: bump toolchain, bye auto pure
2022-02-12 15:09:13 +01:00
00bf10c6f0
chore: bump toolchain
2022-02-09 22:45:28 +01:00
5ef4ead859
Merge branch 'main' into equations
2022-02-05 02:31:00 +01:00
f54c192e6f
feat: equations
...
Equation implementation for definitions, right now lots of definitions
simply dont generate equational lemmata at all so lots are left
without them.
2022-02-04 22:36:34 +01:00
4d63f90449
feat: Custom structure ctors
...
Add the ability to show customly named structure constructors as well
as a little cosmetic change to how structure fields are displayed.
2022-02-02 12:53:04 +01:00
9ac4eb5062
feat: imports, imported by
2022-01-16 14:22:53 +01:00
735bfa35a7
chore: update compiler version
2022-01-15 15:35:52 +01:00
3f1c0ecd77
chore: Update lean-toolchain
2022-01-04 08:24:59 +01:00
5e0956c4b0
feat: Proper linking of all constants
...
Previously constants in function applications where either not linked
at all or linked in a weird way, this change fixes it by making use of
a (as of now umerged) compiler modification as well as Lean.Widget's
TaggedText.
2022-01-03 14:25:50 +01:00
5e5bbe6ffb
chore: Update lean toolchain
2021-12-12 13:38:31 +01:00
c2da7afd76
chore: Update compiler and fix minor breaking change
2021-12-12 13:38:31 +01:00
deb6739fcc
chore: Initial Lake project
2021-12-12 13:37:18 +01:00
Henrik Böving