Skip to content

Instantly share code, notes, and snippets.

Created May 17, 2018 14:55
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)
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