diff options
| author | Son Ho | 2023-12-07 20:52:04 +0100 |
|---|---|---|
| committer | Son Ho | 2023-12-07 20:52:04 +0100 |
| commit | b3ebef29fe3f13a9004b39fcb89afb33fbbfd248 (patch) | |
| tree | a530dfb5c8f45a4a79ce0f03714bb0b90495ee8c /backends/lean/Base/Progress | |
| parent | f7493580421d31b1d3798521b4f9154e69755f89 (diff) | |
Start working on a version of Diverge.FixI more suited to higher-order functions
Diffstat (limited to 'backends/lean/Base/Progress')
| -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 |