Prelude.agda 445 B

12345678910111213141516171819202122232425262728
  1. module Prelude where
  2. infixr 90 _∘_
  3. infixr 0 _$_
  4. id : {A : Set} -> A -> A
  5. id x = x
  6. _∘_ : {A B C : Set} -> (B -> C) -> (A -> B) -> A -> C
  7. (f ∘ g) x = f (g x)
  8. _$_ : {A B : Set} -> (A -> B) -> A -> B
  9. f $ x = f x
  10. flip : {A B C : Set} -> (A -> B -> C) -> B -> A -> C
  11. flip f x y = f y x
  12. const : {A B : Set} -> A -> B -> A
  13. const x _ = x
  14. typeOf : {A : Set} -> A -> Set
  15. typeOf {A} _ = A
  16. typeOf1 : {A : Set1} -> A -> Set1
  17. typeOf1 {A} _ = A