Skip to content

Instantly share code, notes, and snippets.

@canonic-epicure
Created May 9, 2018 13:36
Embed
What would you like to do?
module Language
%default total
mutual
data QuerySource : Type where
Table : (tableName : String) -> QuerySource
SubQuery : Bool -> QuerySource
As : (source : QuerySource) -> {auto prf : QuerySourceIsNotAliased source} -> (aliasName : String) -> QuerySource
data QuerySourceIsNotAliased : QuerySource -> Type where
BecauseItIsTable : QuerySourceIsNotAliased (Table tableName)
BecauseItIsSubquery : QuerySourceIsNotAliased (SubQuery query)
some : QuerySource
some = Table "name" `As` "n"
{-
*Playground> :l Test2.i
/home/nickolay/workspace/Idris/horn/src/Test2.idr:18:1-28:
|
18 | some = Table "name" `As` "n"
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Language.some is possibly not total due to: Language.BecauseItIsTable
*Test2>
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment