]> abstract codata coinductive constructor data do eta-equality field forall hiding import in inductive infix infixl infixr instance interleaved let macro module mutual no-eta-equality open overlap pattern postulate primitive private public quote quoteTerm record renaming rewrite syntax tactic to unquote unquoteDecl unquoteDef using variable where with