
  0 | ||| Operator aliases for some of the functions in
  1 | ||| `Language.Reflection.Syntax`.
  2 | |||
  3 | ||| There are placed in a separate module in order not to
  4 | ||| pollute the envirionment with additional fixity declarations.
  5 | module Language.Reflection.Syntax.Ops
  6 | 
  7 | import Language.Reflection
  8 | import Language.Reflection.Syntax
  9 | 
 10 | %default total
 11 | 
 12 | export infixl 6 .$,.@,.!
 13 | 
 14 | ||| Infix version of `app`
 15 | |||
 16 | ||| Example: ```var "Just" .$ var "x"```
 17 | public export %inline
 18 | (.$) : TTImp -> TTImp -> TTImp
 19 | (.$) = IApp EmptyFC
 20 | 
 21 | ||| Infix version of `namedApp`.
 22 | public export %inline
 23 | (.!) : TTImp -> (Name,TTImp) -> TTImp
 24 | s .! (n,t) = namedApp s n t
 25 | 
 26 | -- Use same fixity as in `Syntax.PreorderReasoning.Generic`
 27 | export infix 1 .=>
 28 | 
 29 | ||| Infix alias for `lam`.
 30 | |||
 31 | ||| @deprecation: This is in conflict with a similar operator from
 32 | ||| `Syntax.PreorderReasoning`. It will be removed in a later commit.
 33 | public export %inline %deprecate
 34 | (.=>) : Arg -> TTImp -> TTImp
 35 | (.=>) = lam
 36 | 
 37 | export infixr 5 .->
 38 | 
 39 | ||| Infix alias for `pi`.
 40 | public export %inline
 41 | (.->) : Arg -> TTImp -> TTImp
 42 | (.->) = pi
 43 | 
 44 | export infixr 3 .=
 45 | 
 46 | ||| Infix alias for `patClause`
 47 | public export %inline
 48 | (.=) : TTImp -> TTImp -> Clause
 49 | (.=) = patClause
 50 |