This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
moduspoens : {P : Set} → {Q : Set} → P → (P → Q) → Q | |
moduspoens p imp = imp p |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
data True : Set where | |
qed : True | |
data False : Set where | |
-- false has no constructors |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
_flatMapOption_ : {A : Set} → {B : Set} → Option A → (A → Option B) → Option B | |
None flatMapOption _ = None | |
(Some a) flatMapOption f = f a |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
_mapOption_ : {A : Set} → {B : Set} → Option A → (A → B) → Option B | |
None mapOption _ = None | |
(Some a) mapOption f = Some (f a) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
_find_ : {A : Set} → List A → (A → Bool) → Option A | |
[] find _ = None | |
(x :: xs) find p = if (p x) then (Some x) else (xs find p) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
data Option (A : Set) : Set where | |
Some : A → Option A | |
None : Option A |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
open import Nat | |
upto : ℕ → List ℕ | |
upto zero = [] | |
upto (succ n) = (upto n) ++ ((succ n) :: []) | |
listsqs : ℕ → List ℕ | |
listsqs n = upto n map (λ x → (x * x)) | |
sumsqs : ℕ → ℕ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
fold_by_from_ : {A : Set} → {B : Set} → List A → (A → B → B) → B → B | |
fold [] by _ from b = b | |
fold (x :: xs) by op from b = op x (fold xs by op from b) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
_filter_ : {A : Set} → List A → (A → Bool) → List A | |
[] filter _ = [] | |
(x :: xs) filter p = if (p x) then (x :: (xs filter p)) else (xs filter p) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
if_then_else : {A : Set} → Bool → A → A → A | |
if true then x else _ = x | |
if false then _ else y = y |