From 3ead2de881fd9d3b7a262acee0699ca2fa1026f0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gabrielle=20Guimar=C3=A3es=20de=20Oliveira?= Date: Thu, 23 Mar 2023 08:45:45 -0300 Subject: [PATCH] docs: fix top level declarations names cases --- README.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 57f4619a..c12505d9 100644 --- a/README.md +++ b/README.md @@ -36,18 +36,18 @@ Pure functions are defined via equations, as in [Haskell](https://www.haskell.or ```javascript // Applies a function to every element of a list -map (list: List a) (f: a -> b) : List b -map a b Nil f = Nil -map a b (Cons head tail) f = Cons (f head) (map tail f) +Map (list: List a) (f: a -> b) : List b +Map a b Nil f = Nil +Map a b (Cons head tail) f = Cons (f head) (Map tail f) ``` Theorems can be proved inductively, as in [Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php) and [Idris](https://www.idris-lang.org/): ```javascript // Black Friday Theorem. Proof that, for every Nat n: n * 2 / 2 == n. -black_friday_theorem (n: Nat) : Equal Nat (Nat.half (Nat.double n)) n -black_friday_theorem Nat.zero = Equal.refl -black_friday_theorem (Nat.succ n) = Equal.apply (x => Nat.succ x) (black_friday_theorem n) +BlackFridayTheorem (n: Nat) : Equal Nat (Nat.half (Nat.double n)) n +BlackFridayTheorem Nat.zero = Equal.refl +BlackFridayTheorem (Nat.succ n) = Equal.apply (x => Nat.succ x) (BlackFridayTheorem n) ``` For more examples, check the [Wikind](https://github.com/kindelia/wikind).