You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The -' and +' functions carry out the same functionality with a different operator. Given multiplication and division operations will require similar logic, it makes sense to abstract this out into a single function with a signature along the lines of ∀ {a} {A : Set a} → Maybe A → Maybe A → (A → A → A) → Maybe A, which takes two Maybe types along with an operator, and applies the operator if and only if both parameters are not nothing. It could be called like so:
maybeOp (⟦ E ⟧ σ) (⟦ E' ⟧ σ) _+_ -- for addition
maybeOp (⟦ E ⟧ σ) (⟦ E' ⟧ σ) _∸_ -- for subtraction
The text was updated successfully, but these errors were encountered:
The
-'
and+'
functions carry out the same functionality with a different operator. Given multiplication and division operations will require similar logic, it makes sense to abstract this out into a single function with a signature along the lines of∀ {a} {A : Set a} → Maybe A → Maybe A → (A → A → A) → Maybe A
, which takes twoMaybe
types along with an operator, and applies the operator if and only if both parameters are notnothing
. It could be called like so:The text was updated successfully, but these errors were encountered: