idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 11:05:17 +03:00
Code Issues Projects Releases Wiki Activity

If we know the types of a & b start searching.

Browse Source 
This is helpful when defining auto-implicits of the form:

    pairEqF : DecEq a
           => (thisX, x, y : a)
           -> {prfRefl : Equal x thisX}
           -> (prfEq   : decEq x thisX = Yes prfRefl)
           => Pair a a
    pairEqF thisX x y {prfRefl} {prfEq} = MkPair x y

before auto-implicit search would fail to find `Refl` for `prfRefl`.
With this fix the solution is found.

This fix means we can avoid having to write the following.

    pairEqF' : DecEq a
            => (thisX, x, y : a)
            -> (prfEq   : decEq x thisX = Yes (the (Equal x x) Refl))
            => Pair a a
    pairEqF' thisX x y {prfEq} = MkPair x y
This commit is contained in:
Jan de Muijnck-Hughes 2020-07-10 16:01:58 +01:00 committed by G. Allais
parent fcbfcf6fe2
commit 5774a9c6ae
1 changed files with 1 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
libs/prelude/Builtin.idr
View File

@ -110,6 +110,7 @@ data Void : Type where
public export
data Equal : forall a, b . a -> b -> Type where
[search a b]
Refl : {0 x : a} -> Equal x x
%name Equal prf