fabian/veribase-idr2 - Change YE3EAD3XYKXRHEJN4VLBVBQM2EISKFHAESPOZ6S4QMLA6YZEVDQQC

Fix `Equiv` signatures to take into account multiple implementations of interface

Co-authored-by: Ohad Kammar <ohad.kammar@gmail.com>

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

YE3EAD3XYKXRHEJN4VLBVBQM2EISKFHAESPOZ6S4QMLA6YZEVDQQC

Dependencies

In channels

main

Change contents

Replacement in src/Data/LinkedList.idr at line 15 [3.17]

B:BD[3.201] → [3.201:372]

data LinkedListEquiv : (a, b : LinkedList t) -> Type where
  BothEmpty : LinkedListEquiv Nil Nil
  EquivHeadAndTail : Equivalence t => {a, b : t} -> {x, y : LinkedList t}

[3.201]

[3.372]

data LinkedListEquiv : Equivalence t => (a, b : LinkedList t) -> Type where
  BothEmpty : (e : Equivalence t) => LinkedListEquiv @{e} Nil Nil
  EquivHeadAndTail : (e : Equivalence t) => {a, b : t} -> {x, y : LinkedList t}

Replacement in src/Data/LinkedList.idr at line 19 [3.17]

B:BD[3.441] → [3.441:497]

                   -> LinkedListEquiv (a :: x) (b :: y)

[3.441]

[3.497]

                   -> LinkedListEquiv @{e} (a :: x) (b :: y)

Replacement in src/Data/LinkedList.idr at line 22 [3.17]

B:BD[3.512] → [3.512:561]

Uninhabited (LinkedListEquiv Nil (h :: t)) where

[3.512]

[3.561]

(e : Equivalence a) => Uninhabited (LinkedListEquiv @{e} Nil (h :: t)) where

Replacement in src/Data/LinkedList.idr at line 27 [3.17]

B:BD[3.659] → [3.659:708]

Uninhabited (LinkedListEquiv (h :: t) Nil) where

[3.659]

[3.708]

(e : Equivalence a) => Uninhabited (LinkedListEquiv @{e} (h :: t) Nil) where

Replacement in src/Data/LinkedList.idr at line 32 [3.17]

B:BD[3.806] → [3.806:921]

fromNotEquivHead : Equivalence t => {a, b : t} -> (ok: Not (Equiv a b)) -> Not (LinkedListEquiv (a :: x) (b :: y))

[3.806]

[3.921]

fromNotEquivHead : (e : Equivalence t) => {a, b : t} -> (ok: Not (Equiv a b))
                 -> Not (LinkedListEquiv @{e} (a :: x) (b :: y))

Replacement in src/Data/LinkedList.idr at line 35 [3.17]

B:BD[3.963] → [3.963:1017]

fromNotEquivHead ctr (EquivHeadAndTail prf _) = ?ctra

[3.963]

[3.1017]

fromNotEquivHead ctr (EquivHeadAndTail prf _) = ctr prf

Replacement in src/Data/LinkedList.idr at line 38 [3.17]

B:BD[3.1032] → [3.1032:1126]

fromNotEquivTail : (ok: Not (LinkedListEquiv x y)) -> Not (LinkedListEquiv (a :: x) (b :: y))

[3.1032]

[3.1126]

fromNotEquivTail : (e : Equivalence t) => (ok: Not (LinkedListEquiv @{e} x y))
                 -> Not (LinkedListEquiv @{e} (a :: x) (b :: y))

Deletion in src/Data/LinkedList.idr at line 42 [3.17]

B:BD[3.1224] → [3.1224:1315]


public export
Equivalence t => Equivalence (LinkedList t) where
  Equiv = LinkedListEquiv

Replacement in src/Data/LinkedList.idr at line 43 [3.17]

B:BD[3.1316] → [3.1316:1505]

  decEquiv Nil Nil = Yes $ BothEmpty
  decEquiv Nil (_ :: _) = No $ absurd
  decEquiv (_ :: _) Nil = No $ absurd
  decEquiv (h1 :: t1) (h2 :: t2) = case (decEquiv h1 h2, decEquiv t1 t2) of

[3.1316]

[3.1505]

decLinkedListEquiv : (e : Equivalence t) => (a, b : LinkedList t) -> Dec (LinkedListEquiv @{e} a b)
decLinkedListEquiv Nil Nil = Yes $ BothEmpty
decLinkedListEquiv Nil (_ :: _) = No $ absurd
decLinkedListEquiv (_ :: _) Nil = No $ absurd
decLinkedListEquiv @{e} (h1 :: t1) (h2 :: t2) = assert_total $
  case (decEquiv @{e} h1 h2, decLinkedListEquiv t1 t2) of

Replacement in src/Data/LinkedList.idr at line 50 [3.17]

B:BD[3.1566] → [3.1566:1718]

    (Yes prf1, No ctra2) => No $ fromNotEquivTail ctra2
    (No ctra1, _) => No $ fromNotEquivHead ctra1
    _ => ?impossibleCase -- TODO: Upstream bug

[3.1566]

[3.1718]

    (Yes prf1, No ctra2) => No $ fromNotEquivTail @{e} ctra2
    (No ctra1, _) => No $ fromNotEquivHead @{e} ctra1
public export
(Equivalence t) => Equivalence (LinkedList t) where
  Equiv    = LinkedListEquiv
  decEquiv = decLinkedListEquiv

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

B:BD[2.999] → [2.999:1196]

data OptionalEquiv : (a, b : Optional t) -> Type where
  BothNothing : OptionalEquiv Nothing Nothing
  BothSame : Equivalence t => {a, b : t} -> (ok : Equiv a b) -> OptionalEquiv (Some a) (Some b)

[2.999]

[2.1196]

data OptionalEquiv : Equivalence t => (a, b : Optional t) -> Type where
  BothNothing : (e : Equivalence t) => OptionalEquiv @{e} Nothing Nothing
  BothSame : (e : Equivalence t) => {a, b : t} -> (ok : Equiv a b)
           -> OptionalEquiv @{e} (Some a) (Some b)

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

B:BD[2.1211] → [2.1211:1262]

Uninhabited (OptionalEquiv Nothing (Some b)) where

[2.1211]

[2.1262]

(e : Equivalence t) => Uninhabited (OptionalEquiv @{e} Nothing (Some b)) where

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

B:BD[2.1353] → [2.1353:1404]

Uninhabited (OptionalEquiv (Some a) Nothing) where

[2.1353]

[2.1404]

(e : Equivalence t) => Uninhabited (OptionalEquiv @{e} (Some a) Nothing) where

Replacement in src/Data/Optional.idr at line 31 [4.30]
B:BD[2.1644] → [2.1644:1683]
```
fromNotEquiv ok (BothSame ctr) = ?ctra
```
[2.1644]
[2.1683]
```
fromNotEquiv ok (BothSame ctr) = ok ctr
```