diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2023-01-12 17:56:11 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2023-01-12 17:56:11 +0000 |
| commit | bfba6b295a8cdf7321d939f22fbdd04d45408e63 (patch) | |
| tree | 21ffcca0da42cebcd911c4007e092c6b68d3d877 | |
| parent | de4275d9728104167726bda4d260c197a40ff3d7 (diff) | |
Fix bug in equality for pi types.
| -rw-r--r-- | src/Obs/NormalForm/Normalise.idr | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Obs/NormalForm/Normalise.idr b/src/Obs/NormalForm/Normalise.idr index 28d66da..3ed0e67 100644 --- a/src/Obs/NormalForm/Normalise.idr +++ b/src/Obs/NormalForm/Normalise.idr @@ -505,7 +505,7 @@ equalHelper let returnElement = Cnstr $ Pi { domainSort = domainSort , codomainSort = Prop - , domain = MkDecl Nothing (Sorted.weaken [Irrelevant] domain.type) + , domain = MkDecl Nothing (Sorted.weaken [Irrelevant] domain'.type) , codomain = codomainEqual } |