mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-24 04:09:10 +03:00
[ new ] Pretty
instance for SizeChange
This commit is contained in:
parent
8a9bf396ea
commit
c4677edc5f
@ -154,3 +154,9 @@ scMultPlusDist a Same Same =
|
||||
scMultPlusDist Smaller Same Smaller = Refl
|
||||
scMultPlusDist Smaller Smaller Same = Refl
|
||||
scMultPlusDist Smaller Smaller Smaller = Refl
|
||||
|
||||
export
|
||||
Pretty Void SizeChange where
|
||||
pretty Smaller = pretty "<"
|
||||
pretty Same = pretty "="
|
||||
pretty Unknown = neutral
|
||||
|
Loading…
Reference in New Issue
Block a user