diff options
| author | Son Ho | 2023-07-17 12:14:03 +0200 |
|---|---|---|
| committer | Son Ho | 2023-07-17 12:14:03 +0200 |
| commit | d45c6ed9e8049b81170c3e6950043d08006ba9f2 (patch) | |
| tree | eb15b4cc1d1d175bf7737d1e12442a4df01e0bc1 /backends/lean/Base/Arith/Arith.lean | |
| parent | 4f7ebc2358d78d31d63a609a32e5a732b82d468e (diff) | |
Move a definition
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base/Arith/Arith.lean | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/backends/lean/Base/Arith/Arith.lean b/backends/lean/Base/Arith/Arith.lean index 8bfad6ae..da263e86 100644 --- a/backends/lean/Base/Arith/Arith.lean +++ b/backends/lean/Base/Arith/Arith.lean @@ -16,9 +16,6 @@ namespace Arith open Primitives Utils -- TODO: move -instance Vec.cast (a : Type): Coe (Vec a) (List a) where coe := λ v => v.val - --- TODO: move /- Remark: we can't write the following instance because of restrictions about the type class parameters (`ty` doesn't appear in the return type, which is forbidden): |