mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-10-26 18:02:24 +03:00
Fix DecEq implementation on primitives
We can't just make up any old proof for the not equal case, since it messes up type checking later! Instead, use a postulate, since we won't do any calculation with it since it produces a Void.
This commit is contained in:
parent
88f5c717d8
commit
3b35e39eb9
@ -157,7 +157,8 @@ implementation DecEq a => DecEq (List a) where
|
||||
|
||||
|
||||
-- For the primitives, we have to cheat because we don't have access to their
|
||||
-- internal implementations.
|
||||
-- internal implementations. We postulate the inequality proofs because we're
|
||||
-- never going to have to compute anything from them.
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Int
|
||||
@ -169,8 +170,7 @@ implementation DecEq Int where
|
||||
False => No primitiveNotEq
|
||||
where primitiveEq : x = y
|
||||
primitiveEq = really_believe_me (Refl {x})
|
||||
primitiveNotEq : x = y -> Void
|
||||
primitiveNotEq = really_believe_me (id {a = x = y})
|
||||
postulate primitiveNotEq : x = y -> Void
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Char
|
||||
@ -182,8 +182,7 @@ implementation DecEq Char where
|
||||
False => No primitiveNotEq
|
||||
where primitiveEq : x = y
|
||||
primitiveEq = really_believe_me (Refl {x})
|
||||
primitiveNotEq : x = y -> Void
|
||||
primitiveNotEq = really_believe_me (id {a = x = y})
|
||||
postulate primitiveNotEq : x = y -> Void
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Integer
|
||||
@ -195,8 +194,7 @@ implementation DecEq Integer where
|
||||
False => No primitiveNotEq
|
||||
where primitiveEq : x = y
|
||||
primitiveEq = really_believe_me (Refl {x})
|
||||
primitiveNotEq : x = y -> Void
|
||||
primitiveNotEq = really_believe_me (id {a = x = y})
|
||||
postulate primitiveNotEq : x = y -> Void
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- String
|
||||
@ -208,8 +206,7 @@ implementation DecEq String where
|
||||
False => No primitiveNotEq
|
||||
where primitiveEq : x = y
|
||||
primitiveEq = really_believe_me (Refl {x})
|
||||
primitiveNotEq : x = y -> Void
|
||||
primitiveNotEq = really_believe_me (id {a = x = y})
|
||||
postulate primitiveNotEq : x = y -> Void
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Ptr
|
||||
@ -221,8 +218,7 @@ implementation DecEq Ptr where
|
||||
False => No primitiveNotEq
|
||||
where primitiveEq : x = y
|
||||
primitiveEq = really_believe_me (Refl {x})
|
||||
primitiveNotEq : x = y -> Void
|
||||
primitiveNotEq = really_believe_me (id {a = x = y})
|
||||
postulate primitiveNotEq : x = y -> Void
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- ManagedPtr
|
||||
@ -234,5 +230,4 @@ implementation DecEq ManagedPtr where
|
||||
False => No primitiveNotEq
|
||||
where primitiveEq : x = y
|
||||
primitiveEq = really_believe_me (Refl {x})
|
||||
primitiveNotEq : x = y -> Void
|
||||
primitiveNotEq = really_believe_me (id {a = x = y})
|
||||
postulate primitiveNotEq : x = y -> Void
|
||||
|
Loading…
Reference in New Issue
Block a user