Skip to content

Instantly share code, notes, and snippets.

@canonic-epicure
Last active May 17, 2018 14:50
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Embed
What would you like to do?
module Language
import Data.So
%default total
-- typechecks after removing "mutual"
mutual
record SomeRec where
constructor MkSomeRec
WhereCondition : Bool
some : (rec : SomeRec) -> {auto so : So (WhereCondition rec)} -> Bool
some rec = ?some_rhs
zz : Bool
zz = some (MkSomeRec True)
{-
Errors (3)
/home/nickolay/workspace/Idris/horn/src/Test2.idr:14:10
When checking type of Language.some:
When checking an application of type constructor Data.So.So:
No such variable WhereCondition
/home/nickolay/workspace/Idris/horn/src/Test2.idr:15:5
No type declaration for Language.some
/home/nickolay/workspace/Idris/horn/src/Test2.idr:18:10
When checking right hand side of zz with expected type
Bool
No such variable some
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment