Skip to content

Instantly share code, notes, and snippets.

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
What would you like to do?
module Language
import Data.So
%default total
-- typechecks after removing "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)
When checking type of Language.some:
When checking an application of type constructor Data.So.So:
No such variable WhereCondition
No type declaration for Language.some
When checking right hand side of zz with expected type
No such variable some
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment