Leonardo de Moura
bbad6d1efe
feat: add with_annotate_term
2022-07-26 15:13:28 -07:00
Leonardo de Moura
f1f5a4b39e
chore: naming convention
2022-07-24 17:44:29 -07:00
Leonardo de Moura
5e877b115b
feat: improve calc tactic
...
> Heather suggested changing the calc tactic (not the term) such that if
the final RHS does not defeq match the goal RHS, it returns a final
inequality as a subgoal.
Closes #1342
2022-07-24 14:30:15 -07:00
Leonardo de Moura
c46ef56ac7
perf: avoid blowup at deriving Repr
...
The fix is not perfect. I just avoided inlining in some builtin `Repr` instances.
The actual problem is at `ElimDeadBranches.lean`.
Closes #1365
2022-07-24 13:10:04 -07:00
Leonardo de Moura
22d37af5c9
feat: improve calc syntax
...
See #1342
2022-07-24 08:32:20 -07:00
Sebastian Ullrich
5160cb7b0f
refactor: remove some unnecessary antiquotation kind annotations
2022-07-23 17:09:32 +02:00
Sebastian Ullrich
cf380956a3
fix: regression from previous commit
2022-07-23 17:09:32 +02:00
Mario Carneiro
f6211b1a74
chore: convert doc/mod comments from /- to /--//-! ( #1354 )
2022-07-22 12:05:31 -07:00
Sebastian Ullrich
1f081ee6cb
feat: doc comment support for unif_hint
2022-07-22 14:30:49 +02:00
Andrés Goens
b36b50adb2
feat: syntax for using while condition in proofs
2022-07-21 16:57:35 +00:00
Henrik Böving
8932878274
feat: Functor instance for List
2022-07-21 08:08:48 -07:00
Ed Ayers
0bfee4fe1f
doc: apply suggestions from code review
...
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
2022-07-20 15:30:30 -07:00
E.W.Ayers
8fe76ba9f4
doc: prelude Nat, Fin, USize
2022-07-20 15:30:30 -07:00
Sebastian Ullrich
cdb855d281
feat: support all sensible modifiers on (builtin_)initialize
...
Resolves #1324
2022-07-20 22:12:20 +02:00
Gabriel Ebner
eda3eae18e
perf: implement Expr.update* in Lean
2022-07-19 05:55:13 -07:00
Leonardo de Moura
e1fc904786
feat: attributes on syntax
...
closes #1321
2022-07-18 23:37:11 -04:00
Leonardo de Moura
d95163641a
chore: indent docstrings
2022-07-18 22:36:55 -04:00
Leonardo de Moura
c341d8432f
feat: remove leading spaces from docstrings
2022-07-18 22:18:15 -04:00
Leonardo de Moura
5083d47e4d
doc: some Syntax
2022-07-17 17:57:33 -04:00
Leonardo de Moura
fdef55339f
fix: use binop% for elaborating ^
...
closes #1298
2022-07-12 18:20:02 -07:00
Gabriel Ebner
eba400543d
refactor: use computed fields for Name
2022-07-11 14:19:41 -07:00
Gabriel Ebner
c100f45b77
feat: add simp lemmas and instances for LawfulBEq
2022-07-11 14:19:41 -07:00
Gabriel Ebner
3776e3c925
feat: generalize unsafeCast to Sort
2022-07-11 12:26:53 -07:00
Leonardo de Moura
2fcd406f99
chore: remove sorry
2022-07-10 20:04:06 -07:00
Leonardo de Moura
ee0735760a
feat: add instance : GetElem (List α) Nat α fun as i => i < as.length
2022-07-10 17:38:59 -07:00
Leonardo de Moura
475c7e18cd
chore: missing GetElem instances
2022-07-10 14:53:22 -07:00
Leonardo de Moura
4173a863d8
chore: cleanup
2022-07-10 09:43:12 -07:00
Leonardo de Moura
4b543d5edd
feat: add option for disabling dsimp during simp
2022-07-10 07:57:41 -07:00
Leonardo de Moura
2f1b80721e
chore: avoid a[i]' h notation
2022-07-10 07:20:07 -07:00
Leonardo de Moura
35018dbea2
feat: unexpanders for a[i], a[i]' h, a[i]!, and a[i]?
2022-07-10 06:47:23 -07:00
Leonardo de Moura
881589fc46
chore: remove parser workarounds
2022-07-09 16:42:39 -07:00
Leonardo de Moura
aa52eebcdc
feat: add instance GetElem (Array α) USize α fun xs i => LT.lt i.toNat xs.size where
2022-07-09 16:18:29 -07:00
Leonardo de Moura
1caff852fb
chore: remove getOp functions
2022-07-09 16:09:28 -07:00
Leonardo de Moura
36ebccb822
chore: fix tests
2022-07-09 15:59:44 -07:00
Leonardo de Moura
e4b358a01e
refactor: prepare to elaborate a[i] notation using typeclasses
2022-07-09 15:24:22 -07:00
Leonardo de Moura
4c707d3b3c
feat: use binop% to elaborate %-applications
...
Motivation: make sure the behavior is consistent with other arithmetic
operators.
This commit also removes the instance
```
instance : HMod (Fin n) Nat (Fin n) where
hMod := Fin.modn
```
because we have a coercion from `Fin n` to `Nat`.
Thus, given `a : Fin n` and `b : Nat`, `a % b` is ambiguous.
2022-07-09 14:38:35 -07:00
Leonardo de Moura
c9771fa1b2
chore: unused variables
2022-07-07 20:24:18 -07:00
Leonardo de Moura
dd924e5270
chore: remove codegen option
...
We should use `noncomputable` modifier instead.
closes #1288
2022-07-07 08:18:30 -07:00
Leonardo de Moura
2b2d4245dc
fix: extensible tactics bug
...
See comment at `expandMacros`
2022-07-05 13:20:22 -07:00
tydeu
bff560759e
feat: add missing literal TSyntax helpers
2022-07-05 13:18:58 +02:00
Leonardo de Moura
757171db1f
feat: add String.get! and s[i]! notation for String
2022-07-03 14:59:44 -07:00
Gabriel Ebner
141b110ff1
feat: add more typed syntax coercions
2022-07-03 22:46:59 +02:00
Gabriel Ebner
922ef23112
fix: do not ignore syntax coercions
...
Syntax coercions do not need to be the identity. See for example
``Coe (TSyntax `ident) (TSyntax `declId)``.
2022-07-03 22:46:59 +02:00
Gabriel Ebner
ddf77a8c6d
chore: style
2022-07-03 22:46:59 +02:00
Gabriel Ebner
bec0bbc351
fix: replace dangerous instance by CoeTail
...
In order to guarantee termination of type class synthesis when resolving
coercions, a good rule of thumb is that the instances should not
introduce metavariables (during TC synthesis). For common coercion type
classes this means:
- `Coe T S`, `CoeTail T S`: the variables of `T` must be a subset of those of `S`
- `CoeHead T S`: the variables of `S` must be a subset of those of `T`
If these rules are not followed, we can easily get nontermination. In
this case: `CoeTC Foo Syntax` is reduced to `CoeTC Foo (TSyntax ?m_1)`
using the (dangerous) `Coe (TSyntax k) Syntax` instance, to which we can
then apply the otherwise fine `Coe (TSyntax [k]) (TSyntax (k'::ks))`
coercion infinitely often.
2022-07-03 22:46:59 +02:00
Gabriel Ebner
3d5c5553d9
fix: add missing coercion instance for CoeHead+CoeTail
2022-07-03 22:46:59 +02:00
Leonardo de Moura
5e3a3a6c21
chore: remove notation a[i,h] for a[⟨i, h⟩]
2022-07-03 06:24:26 -07:00
Leonardo de Moura
54c60d4c2d
feat: a[i] and a[i]! notation for Subarrays
2022-07-02 15:54:34 -07:00
Leonardo de Moura
a2456c3a0f
feat: add notation a[i, h] for a[⟨i, h⟩]
2022-07-02 15:50:49 -07:00
Leonardo de Moura
b3ea1fc925
feat: a[i] notation for arrays now uses i : Fin a.size
2022-07-02 15:19:38 -07:00
