diff options
Diffstat (limited to 'backends/lean/Base/Progress/Base.lean')
| -rw-r--r-- | backends/lean/Base/Progress/Base.lean | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean index cf2a3b70..573f0cc5 100644 --- a/backends/lean/Base/Progress/Base.lean +++ b/backends/lean/Base/Progress/Base.lean @@ -154,6 +154,7 @@ structure PSpecAttr where specs of the scalar operations, which is what I really need, but I'm not sure it applies well to other situations. A better way would probably to use type classes, but I couldn't get them to work on those cases. It is worth retrying. + UPDATE: use discrimination trees (`DiscrTree`) from core Lean -/ structure PSpecClassAttr where attr : AttributeImpl |