------------------------------------------------------------------------
-- 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 0 ∋-syntax
∋-syntax = _∋_
-- Create ∶ syntax
syntax ∋-syntax A a = a ∶ A
-- Export pipeline functions
open import Function.Base public using (_|>_; _|>′_)
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