------------------------------------------------------------------------
-- The Agda standard library
--
-- Monad syntax for the TC monad
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Reflection.TCM.Syntax where
open import Agda.Builtin.Reflection
open import Level using (Level)
private
variable
a b : Level
A : Set a
B : Set b
------------------------------------------------------------------------
-- Monad syntax
infixl 3 _<|>_
_<|>_ : TC A → TC A → TC A
_<|>_ = catchTC
{-# INLINE _<|>_ #-}
infixl 1 _>>=_ _>>_ _<&>_
_>>=_ : TC A → (A → TC B) → TC B
_>>=_ = bindTC
{-# INLINE _>>=_ #-}
_>>_ : TC A → TC B → TC B
xs >> ys = bindTC xs (λ _ → ys)
{-# INLINE _>>_ #-}
infixl 4 _<$>_ _<*>_ _<$_
_<*>_ : TC (A → B) → TC A → TC B
fs <*> xs = bindTC fs (λ f → bindTC xs (λ x → returnTC (f x)))
{-# INLINE _<*>_ #-}
_<$>_ : (A → B) → TC A → TC B
f <$> xs = bindTC xs (λ x → returnTC (f x))
{-# INLINE _<$>_ #-}
_<$_ : A → TC B → TC A
x <$ xs = bindTC xs (λ _ → returnTC x)
{-# INLINE _<$_ #-}
_<&>_ : TC A → (A → B) → TC B
xs <&> f = bindTC xs (λ x → returnTC (f x))
{-# INLINE _<&>_ #-}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4