fabian/veribase-idr2 - Change ZQLW6BX54QFHXQHJTOQ7KW3TBNE6VZZGTD3FPUOLVULYRS66NGLQC

Refactor to simplify Optional's decEquiv

Created by Fabián Heredia Montiel on May 24, 2021

ZQLW6BX54QFHXQHJTOQ7KW3TBNE6VZZGTD3FPUOLVULYRS66NGLQC

Dependencies

[2] 7SFN5S4CUZZL523G6RHETVEJCJUIMXH2YPDTRKQWCGZTDYNWW4LQC
[3] 6D4TYQRJMN6QEKASHJ3ZN3E7TXF5IEQ3G4ATTZZ5AZC56VXMWFZAC
[4] XNPLRKJ4ZK442XNJ5BC7TO3DKXGXFSOSGBZBPW5HZZDHY3IVD6FAC

In channels

main

Change contents

Replacement in src/Data/Optional.idr at line 39 [4.30]

B:BD[3.1906] → [3.1906:2087]

  decEquiv (Some a) (Some b) with (decEquiv a b)
    decEquiv (Some a) (Some b) | (Yes prf) = Yes $ BothSame prf
    decEquiv (Some a) (Some b) | (No ctra) = No $ fromNotEquiv ctra

[3.1906]

[2.342]

  decEquiv (Some a) (Some b) = case (decEquiv a b) of
    (Yes prf) => Yes $ BothSame prf
    (No ctra) => No $ fromNotEquiv ctra