Skip to content

Instantly share code, notes, and snippets.

@canonic-epicure
Created May 17, 2018 14:55
Embed
What would you like to do?
module Language
import Data.So
%default total
record SomeRec where
constructor MkSomeRec
WhereCondition : Bool
some : (rec : SomeRec) -> {auto so : So (Language.WhereCondition rec)} -> Bool
some rec = ?some_rhs
zz : Bool
zz = some (MkSomeRec True)
{-
Errors (1)
/home/nickolay/workspace/Idris/horn/src/Test2.idr:12:6
When checking type of Language.some:
When checking an application of type constructor Data.So.So:
No such variable Language.WhereCondition
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment