Skip to content

Commit

Permalink
drop accidental unicode
Browse files Browse the repository at this point in the history
  • Loading branch information
lemastero committed Jun 25, 2022
1 parent 7baee99 commit 0fef09a
Showing 1 changed file with 8 additions and 8 deletions.
16 changes: 8 additions & 8 deletions src/Data/Can/Properties.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,13 +81,13 @@ module _ {la lb} {A : Set la} {B : Set lb} where
(deca a1 a2 *-dec decb b1 b2)
≡-dec deca decb non (one a) = no \ ()
≡-dec deca decb non (eno b) = no \ ()
≡-dec deca decb non (two a b) = no \ ()
≡-dec deca decb (one a) non = no \ ()
≡-dec deca decb (one a) (eno b) = no \ ()
≡-dec deca decb (one a1) (two a2 b2) = no \ ()
≡-dec deca decb non (two a b) = no \ ()
≡-dec deca decb (one a) non = no \ ()
≡-dec deca decb (one a) (eno b) = no \ ()
≡-dec deca decb (one a1) (two a2 b2) = no \ ()
≡-dec deca decb (eno b) non = no \ ()
≡-dec deca decb (eno b) (one a) = no \ ()
≡-dec deca decb (eno b1) (two a b2) = no \ ()
≡-dec deca decb (two a b) non = no \ ()
≡-dec deca decb (two a1 b) (one a2) = no \ ()
≡-dec deca decb (two a b1) (eno b2) = no \ ()
≡-dec deca decb (eno b1) (two a b2) = no \ ()
≡-dec deca decb (two a b) non = no \ ()
≡-dec deca decb (two a1 b) (one a2) = no \ ()
≡-dec deca decb (two a b1) (eno b2) = no \ ()

0 comments on commit 0fef09a

Please sign in to comment.