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
Leonardo de Moura
2ebcf29cde
chore: use a[i]! for array accesses that may panic
2022-07-02 15:12:05 -07:00
Leonardo de Moura
3f3cd22366
feat: add Array.getOp! and Array.getOp?
...
Add warning when `Array.getOp` is used. TODO: replace `Array.getOp`
with safe version
2022-07-02 10:06:05 -07:00
Leonardo de Moura
e8935d996b
chore: String.get?, String.getOp?, and remove String.getOp
2022-07-02 09:59:04 -07:00
Leonardo de Moura
5294a39ec4
feat: add Float.ceil, Float.floor, and Float.round
2022-07-01 06:27:30 -07:00
Leonardo de Moura
fc7c1d1053
chore: remove unnecessary set_option
2022-06-28 17:37:10 -07:00
Sebastian Ullrich
99f5e94efe
feat: MonadExcept.ofExcept
2022-06-28 16:54:29 -07:00
Sebastian Ullrich
9816331562
chore: clean up bootstrapping cleanup
2022-06-28 16:28:36 +02:00
Sebastian Ullrich
77c6f433c7
chore: clean up bootstrapping workarounds
2022-06-28 16:01:07 +02:00
Sebastian Ullrich
89a101e9b8
refactor: remove group(·)s
2022-06-28 11:50:59 +02:00
Leonardo de Moura
34dc2572f3
fix: make sure OfScientific Float instance is never unfolded during type class resolution
...
This commit fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/deterministic.20timeout/near/287654818
Type class resolution was diverging when trying to synthesize
```lean
HSub (optParam Float 0.0) (optParam Float 1.0) ?m.472
```
and Lean was diverging while unfolding
```lean
instance : OfScientific Float where
ofScientific m s e :=
if s then
let s := 64 - m.log2 -- ensure we have 64 bits of mantissa left after division
let m := (m <<< (3 * e + s)) / 5^e
Float.ofBinaryScientific m (-4 * e - s)
else
Float.ofBinaryScientific (m * 5^e) e
```
was being unfolded.
Anothe potential solution for the problem above is to erase the
`optParam` annotations before performing type class resolution.
2022-06-27 17:40:34 -07:00
Sebastian Ullrich
19c2644d88
chore: add more comments
2022-06-27 22:37:02 +02:00
Sebastian Ullrich
22475b8669
refactor: introduce common TSyntax abbreviations
2022-06-27 22:37:02 +02:00
Sebastian Ullrich
e47f248161
doc: TSyntax
2022-06-27 22:37:02 +02:00
Sebastian Ullrich
8b4d8b8dc9
feat: TSyntax singleton kind unexpanders
2022-06-27 22:37:02 +02:00
Sebastian Ullrich
6af00ff23e
chore: changes to placate coercions
2022-06-27 22:37:02 +02:00
Sebastian Ullrich
d9cfda4893
refactor: make more use of quotations
...
Automatically fixes many TSyntax type errors
2022-06-27 22:37:02 +02:00
Sebastian Ullrich
5e334b3e90
chore: postpone TSyntax adoption for some parts
...
The namespace `TSyntax.Compat` can be opened for a coercion
`Syntax -> TSyntax k` for any `k`, as otherwise this PR would never be done.
2022-06-27 22:37:02 +02:00
Sebastian Ullrich
fe22d84143
fix: unclear TSyntax breakage
2022-06-27 22:37:02 +02:00
