Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- 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
- -}
Add Comment
Please, Sign In to add comment