Skip to content

Commit

Permalink
[ fix ] Fix coverage issue (#74)
Browse files Browse the repository at this point in the history
* [ fix ] Fix coverage issue

* Use Uninhabited instead of with
  • Loading branch information
dunhamsteve authored Oct 8, 2024
1 parent 7bffa5c commit 213e508
Showing 1 changed file with 8 additions and 2 deletions.
10 changes: 8 additions & 2 deletions src/Frexlet/Monoid/Frex/Structure.idr
Original file line number Diff line number Diff line change
Expand Up @@ -145,6 +145,12 @@ UltListSetoid pen ult = MkSetoid (UltList (U pen) (U ult)) $ MkEquivalence
, transitive = UltListTransitive pen ult
}

Uninhabited (UltListEquality penRel ultRel (Ultimate i) (ConsUlt j1 y js)) where
uninhabited _ impossible

Uninhabited (UltListEquality penRel ultRel (ConsUlt i1 x is) (Ultimate j)) where
uninhabited _ impossible

public export
MultHomomorphism : (a : Monoid) -> (s : Setoid) ->
SetoidHomomorphism
Expand All @@ -159,8 +165,8 @@ MultHomomorphism a s (i, ConsUlt i1 x is) (j,ConsUlt j1 y js)
= ( a.cong 2 (Dyn 0 .*. Dyn 1) [_,_] [_,_] [i_eq_j, i1_eq_i2]
, x_eq_y
) :: is_eq_js
MultHomomorphism _ _ (_, Ultimate _) (_, ConsUlt _ _ _) (MkAnd _ _) impossible
MultHomomorphism _ _ (_, ConsUlt _ _ _) (_, Ultimate _) (MkAnd _ _) impossible
MultHomomorphism _ _ (_, Ultimate _) (_, ConsUlt _ _ _) (MkAnd _ eq) = absurd eq
MultHomomorphism _ _ (_, ConsUlt _ _ _) (_, Ultimate _) (MkAnd _ eq) = absurd eq

public export
AppendHomomorphismProperty : (a : Monoid) -> (x : Setoid) ->
Expand Down

0 comments on commit 213e508

Please sign in to comment.