------------------------------------------------------------------------
-- The Agda standard library
--
-- A module used for creating function pipelines, see
-- README.Function.Reasoning for examples
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Function.Reasoning where
 
open import Function.Base using (_∋_)
 
-- Need to give _∋_ a new name as syntax cannot contain underscores
infixl  ∋-syntax
∋-syntax = _∋_
 
-- Create ∶ syntax
syntax ∋-syntax A a = a ∶ A
 
-- Export pipeline functions
open import Function.Base public using (_|>_; _|>′_)