mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-22 14:38:20 +03:00
Add Eq instance for Universe in reflection
This commit is contained in:
parent
82c2735637
commit
cf6c277715
@ -242,6 +242,12 @@ instance Eq TT where
|
||||
equalp (TType u) (TType u') = u == u'
|
||||
equalp x y = False
|
||||
|
||||
instance Eq Universe where
|
||||
Reflection.NullType == Reflection.NullType = True
|
||||
Reflection.UniqueType == Reflection.UniqueType = True
|
||||
Reflection.AllTypes == Reflection.AllTypes = True
|
||||
_ == _ = False
|
||||
|
||||
total
|
||||
forget : TT -> Maybe Raw
|
||||
forget tm = fe [] tm
|
||||
|
Loading…
Reference in New Issue
Block a user