diff --git a/exercises/practice/acronym/Acronym.lean b/exercises/practice/acronym/Acronym.lean index 8f094c9..3cc01b5 100644 --- a/exercises/practice/acronym/Acronym.lean +++ b/exercises/practice/acronym/Acronym.lean @@ -1,6 +1,6 @@ namespace Acronym def abbreviate (phrase : String) : String := - sorry + sorry --remove this line and implement the function end Acronym diff --git a/exercises/practice/affine-cipher/AffineCipher.lean b/exercises/practice/affine-cipher/AffineCipher.lean index df672d4..b92a390 100644 --- a/exercises/practice/affine-cipher/AffineCipher.lean +++ b/exercises/practice/affine-cipher/AffineCipher.lean @@ -1,9 +1,9 @@ namespace AffineCipher def encode (phrase : String) (a : Nat) (b : Nat) : Option String := - sorry + sorry --remove this line and implement the function def decode (phrase : String) (a : Nat) (b : Nat) : Option String := - sorry + sorry --remove this line and implement the function end AffineCipher diff --git a/exercises/practice/all-your-base/AllYourBase.lean b/exercises/practice/all-your-base/AllYourBase.lean index 0ea4580..363cbf1 100644 --- a/exercises/practice/all-your-base/AllYourBase.lean +++ b/exercises/practice/all-your-base/AllYourBase.lean @@ -3,6 +3,6 @@ namespace AllYourBase def ValidBase := { x : Nat // x >= 2 } def rebase (inputBase : ValidBase) (digits : List (Fin inputBase.val)) (outputBase : ValidBase) : List (Fin outputBase.val) := - sorry + sorry --remove this line and implement the function end AllYourBase diff --git a/exercises/practice/allergies/Allergies.lean b/exercises/practice/allergies/Allergies.lean index f580596..d61cc7b 100644 --- a/exercises/practice/allergies/Allergies.lean +++ b/exercises/practice/allergies/Allergies.lean @@ -12,9 +12,9 @@ inductive Allergen where deriving BEq, Repr def allergicTo (allergen : Allergen) (score : Nat) : Bool := - sorry + sorry --remove this line and implement the function def list (score : Nat) : List Allergen := - sorry + sorry --remove this line and implement the function end Allergies diff --git a/exercises/practice/anagram/Anagram.lean b/exercises/practice/anagram/Anagram.lean index a7a08c3..3d735d7 100644 --- a/exercises/practice/anagram/Anagram.lean +++ b/exercises/practice/anagram/Anagram.lean @@ -1,6 +1,6 @@ namespace Anagram def findAnagrams (subject : String) : List String -> List String := - sorry + sorry --remove this line and implement the function end Anagram diff --git a/exercises/practice/armstrong-numbers/ArmstrongNumbers.lean b/exercises/practice/armstrong-numbers/ArmstrongNumbers.lean index a4977d5..05a7fee 100644 --- a/exercises/practice/armstrong-numbers/ArmstrongNumbers.lean +++ b/exercises/practice/armstrong-numbers/ArmstrongNumbers.lean @@ -1,6 +1,6 @@ namespace ArmstrongNumbers def isArmstrongNumber (number : Nat) : Bool := - sorry + sorry --remove this line and implement the function end ArmstrongNumbers diff --git a/exercises/practice/atbash-cipher/AtbashCipher.lean b/exercises/practice/atbash-cipher/AtbashCipher.lean index 8b30284..0e42f4e 100644 --- a/exercises/practice/atbash-cipher/AtbashCipher.lean +++ b/exercises/practice/atbash-cipher/AtbashCipher.lean @@ -1,9 +1,9 @@ namespace AtbashCipher def encode (phrase : String) : String := - sorry + sorry --remove this line and implement the function def decode (phrase : String) : String := - sorry + sorry --remove this line and implement the function end AtbashCipher diff --git a/exercises/practice/bank-account/BankAccount.lean b/exercises/practice/bank-account/BankAccount.lean index eb4daa4..96d1ef0 100644 --- a/exercises/practice/bank-account/BankAccount.lean +++ b/exercises/practice/bank-account/BankAccount.lean @@ -5,21 +5,21 @@ structure Account where -- it must be able to handle parallel transactions def Account.create : IO Account := - sorry + sorry --remove this line and implement the function def Account.open (account : Account) : IO Unit := - sorry + sorry --remove this line and implement the function def Account.close (account : Account) : IO Unit := - sorry + sorry --remove this line and implement the function def Account.deposit (amount : Nat) (account : Account) : IO Unit := - sorry + sorry --remove this line and implement the function def Account.withdraw (amount : Nat) (account : Account) : IO Unit := - sorry + sorry --remove this line and implement the function def Account.balance (account : Account) : IO Nat := - sorry + sorry --remove this line and implement the function end BankAccount diff --git a/exercises/practice/binary-search/BinarySearch.lean b/exercises/practice/binary-search/BinarySearch.lean index 955aae5..398f319 100644 --- a/exercises/practice/binary-search/BinarySearch.lean +++ b/exercises/practice/binary-search/BinarySearch.lean @@ -1,6 +1,6 @@ namespace BinarySearch def find (value : Int) (array : Array Int) : Option Nat := - sorry + sorry --remove this line and implement the function end BinarySearch diff --git a/exercises/practice/bob/Bob.lean b/exercises/practice/bob/Bob.lean index 6ac716a..0da6e47 100644 --- a/exercises/practice/bob/Bob.lean +++ b/exercises/practice/bob/Bob.lean @@ -1,6 +1,6 @@ namespace Bob def response (heyBob : String) : String := - sorry + sorry --remove this line and implement the function end Bob diff --git a/exercises/practice/book-store/BookStore.lean b/exercises/practice/book-store/BookStore.lean index 718012a..aa75c23 100644 --- a/exercises/practice/book-store/BookStore.lean +++ b/exercises/practice/book-store/BookStore.lean @@ -3,6 +3,6 @@ namespace BookStore def Book := { x : Nat // x ≥ 1 ∧ x ≤ 5 } def total (basket : List Book) : Nat := - sorry + sorry --remove this line and implement the function end BookStore diff --git a/exercises/practice/camicia/Camicia.lean b/exercises/practice/camicia/Camicia.lean index 85af0ba..e7cf482 100644 --- a/exercises/practice/camicia/Camicia.lean +++ b/exercises/practice/camicia/Camicia.lean @@ -16,6 +16,6 @@ structure Result where deriving BEq, Repr def simulateGame (playerA playerB : List Card) : Result := - sorry + sorry --remove this line and implement the function end Camicia diff --git a/exercises/practice/change/Change.lean b/exercises/practice/change/Change.lean index d7ef09c..c5dd98b 100644 --- a/exercises/practice/change/Change.lean +++ b/exercises/practice/change/Change.lean @@ -6,6 +6,6 @@ inductive Result where deriving BEq, Repr def findFewestCoins (coins : Array Nat) (target : Int) : Result := - sorry + sorry --remove this line and implement the function end Change diff --git a/exercises/practice/clock/Clock.lean b/exercises/practice/clock/Clock.lean index aa9b028..22161f3 100644 --- a/exercises/practice/clock/Clock.lean +++ b/exercises/practice/clock/Clock.lean @@ -5,19 +5,21 @@ structure Clock where -- define equality between Clocks instance : BEq Clock where - beq clock1 clock2 := sorry + beq clock1 clock2 := + sorry --remove this line and implement the function -- define how a Clock should be converted to a String instance : ToString Clock where - toString clock := sorry + toString clock := + sorry --remove this line and implement the function def create (hour : Int) (minute : Int) : Clock := - sorry + sorry --remove this line and implement the function def add (clock : Clock) (minute : Int) : Clock := - sorry + sorry --remove this line and implement the function def subtract (clock : Clock) (minute : Int) : Clock := - sorry + sorry --remove this line and implement the function end Clock diff --git a/exercises/practice/collatz-conjecture/CollatzConjecture.lean b/exercises/practice/collatz-conjecture/CollatzConjecture.lean index fbd925e..9c849c5 100644 --- a/exercises/practice/collatz-conjecture/CollatzConjecture.lean +++ b/exercises/practice/collatz-conjecture/CollatzConjecture.lean @@ -3,6 +3,6 @@ namespace CollatzConjecture def Positive := { x : Nat // 0 < x } def steps (n : Positive) : Nat := - sorry + sorry --remove this line and implement the function end CollatzConjecture diff --git a/exercises/practice/complex-numbers/ComplexNumbers.lean b/exercises/practice/complex-numbers/ComplexNumbers.lean index bf458b2..2287298 100644 --- a/exercises/practice/complex-numbers/ComplexNumbers.lean +++ b/exercises/practice/complex-numbers/ComplexNumbers.lean @@ -7,33 +7,34 @@ structure ComplexNumber where /- define how a complex number should be constructed out of a literal number -/ instance {n : Nat} : OfNat ComplexNumber n where - ofNat := sorry + ofNat := + sorry --remove this line and implement the function def real (z : ComplexNumber) : Float := - sorry + sorry --remove this line and implement the function def imaginary (z : ComplexNumber) : Float := - sorry + sorry --remove this line and implement the function def mul (z1 : ComplexNumber) (z2 : ComplexNumber) : ComplexNumber := - sorry + sorry --remove this line and implement the function def div (z1 : ComplexNumber) (z2 : ComplexNumber) : ComplexNumber := - sorry + sorry --remove this line and implement the function def sub (z1 : ComplexNumber) (z2 : ComplexNumber) : ComplexNumber := - sorry + sorry --remove this line and implement the function def add (z1 : ComplexNumber) (z2 : ComplexNumber) : ComplexNumber := - sorry + sorry --remove this line and implement the function def abs (z : ComplexNumber) : Float := - sorry + sorry --remove this line and implement the function def conjugate (z : ComplexNumber) : ComplexNumber := - sorry + sorry --remove this line and implement the function def exp (z : ComplexNumber) : ComplexNumber := - sorry + sorry --remove this line and implement the function end ComplexNumbers diff --git a/exercises/practice/connect/Connect.lean b/exercises/practice/connect/Connect.lean index 7ef7e28..31bf633 100644 --- a/exercises/practice/connect/Connect.lean +++ b/exercises/practice/connect/Connect.lean @@ -1,6 +1,6 @@ namespace Connect def winner (board : Array String) : Char := - sorry + sorry --remove this line and implement the function end Connect diff --git a/exercises/practice/crypto-square/CryptoSquare.lean b/exercises/practice/crypto-square/CryptoSquare.lean index abe9782..e959368 100644 --- a/exercises/practice/crypto-square/CryptoSquare.lean +++ b/exercises/practice/crypto-square/CryptoSquare.lean @@ -1,6 +1,6 @@ namespace CryptoSquare def ciphertext (plaintext : String) : String := - sorry + sorry --remove this line and implement the function end CryptoSquare diff --git a/exercises/practice/darts/Darts.lean b/exercises/practice/darts/Darts.lean index d46f9b2..beccb19 100644 --- a/exercises/practice/darts/Darts.lean +++ b/exercises/practice/darts/Darts.lean @@ -1,6 +1,6 @@ namespace Darts def score (x : Float) (y : Float) : Int := - sorry + sorry --remove this line and implement the function end Darts diff --git a/exercises/practice/diamond/Diamond.lean b/exercises/practice/diamond/Diamond.lean index 3584b05..c8233f5 100644 --- a/exercises/practice/diamond/Diamond.lean +++ b/exercises/practice/diamond/Diamond.lean @@ -1,6 +1,6 @@ namespace Diamond def rows (letter : Char) : List String := - sorry + sorry --remove this line and implement the function end Diamond diff --git a/exercises/practice/difference-of-squares/DifferenceOfSquares.lean b/exercises/practice/difference-of-squares/DifferenceOfSquares.lean index 29ab458..dce1b9d 100644 --- a/exercises/practice/difference-of-squares/DifferenceOfSquares.lean +++ b/exercises/practice/difference-of-squares/DifferenceOfSquares.lean @@ -1,12 +1,12 @@ namespace DifferenceOfSquares def squareOfSum (number : Nat) : Nat := - sorry + sorry --remove this line and implement the function def sumOfSquares (number : Nat) : Nat := - sorry + sorry --remove this line and implement the function def differenceOfSquares (number : Nat) : Nat := - sorry + sorry --remove this line and implement the function end DifferenceOfSquares diff --git a/exercises/practice/dnd-character/DndCharacter.lean b/exercises/practice/dnd-character/DndCharacter.lean index 3eb22a5..5d15066 100644 --- a/exercises/practice/dnd-character/DndCharacter.lean +++ b/exercises/practice/dnd-character/DndCharacter.lean @@ -10,12 +10,12 @@ structure Character where hitpoints : Int def modifier (score : Nat) : Int := - sorry + sorry --remove this line and implement the function def ability {α} [RandomGen α] (generator : α) : (Nat × α) := - sorry + sorry --remove this line and implement the function def Character.new {α} [RandomGen α] (generator : α) : (Character × α) := - sorry + sorry --remove this line and implement the function end DndCharacter diff --git a/exercises/practice/dominoes/Dominoes.lean b/exercises/practice/dominoes/Dominoes.lean index bb2943e..c0f583f 100644 --- a/exercises/practice/dominoes/Dominoes.lean +++ b/exercises/practice/dominoes/Dominoes.lean @@ -5,6 +5,6 @@ def Half := { x : Nat // x ≥ 1 ∧ x ≤ 6 } def Stone := Half × Half def canChain (dominoes : List Stone) : Bool := - sorry + sorry --remove this line and implement the function end Dominoes diff --git a/exercises/practice/eliuds-eggs/EliudsEggs.lean b/exercises/practice/eliuds-eggs/EliudsEggs.lean index 64117f8..9cea147 100644 --- a/exercises/practice/eliuds-eggs/EliudsEggs.lean +++ b/exercises/practice/eliuds-eggs/EliudsEggs.lean @@ -1,6 +1,6 @@ namespace EliudsEggs def eggCount (number : Nat) : Nat := - sorry + sorry --remove this line and implement the function end EliudsEggs diff --git a/exercises/practice/etl/Etl.lean b/exercises/practice/etl/Etl.lean index 1d08466..9eeb471 100644 --- a/exercises/practice/etl/Etl.lean +++ b/exercises/practice/etl/Etl.lean @@ -3,6 +3,6 @@ import Std namespace Etl def transform (legacy : Std.HashMap Nat (List Char)) : Std.HashMap Char Nat := - sorry + sorry --remove this line and implement the function end Etl diff --git a/exercises/practice/flatten-array/FlattenArray.lean b/exercises/practice/flatten-array/FlattenArray.lean index 96fb5c3..2857e2d 100644 --- a/exercises/practice/flatten-array/FlattenArray.lean +++ b/exercises/practice/flatten-array/FlattenArray.lean @@ -6,6 +6,6 @@ inductive Box (α : Type) : Type where | many (boxes : Array (Box α)) def flatten (box : Box Int) : Array Int := - sorry + sorry --remove this line and implement the function end FlattenArray diff --git a/exercises/practice/forth/Forth.lean b/exercises/practice/forth/Forth.lean index 6ff99f3..18c3e11 100644 --- a/exercises/practice/forth/Forth.lean +++ b/exercises/practice/forth/Forth.lean @@ -1,6 +1,6 @@ namespace Forth def evaluate (instructions : List String) : Except String (List Int) := - sorry + sorry --remove this line and implement the function end Forth diff --git a/exercises/practice/game-of-life/GameOfLife.lean b/exercises/practice/game-of-life/GameOfLife.lean index 8982d67..0720663 100644 --- a/exercises/practice/game-of-life/GameOfLife.lean +++ b/exercises/practice/game-of-life/GameOfLife.lean @@ -1,6 +1,6 @@ namespace GameOfLife def tick (matrix : Array (Array Bool)) : Array (Array Bool) := - sorry + sorry --remove this line and implement the function end GameOfLife diff --git a/exercises/practice/gigasecond/Gigasecond.lean b/exercises/practice/gigasecond/Gigasecond.lean index d498bda..859f6b7 100644 --- a/exercises/practice/gigasecond/Gigasecond.lean +++ b/exercises/practice/gigasecond/Gigasecond.lean @@ -3,6 +3,6 @@ import Std.Time namespace Gigasecond def add (moment : Std.Time.PlainDateTime) : Std.Time.PlainDateTime := - sorry + sorry --remove this line and implement the function end Gigasecond diff --git a/exercises/practice/grains/Grains.lean b/exercises/practice/grains/Grains.lean index 64e4cca..1647e1b 100644 --- a/exercises/practice/grains/Grains.lean +++ b/exercises/practice/grains/Grains.lean @@ -1,9 +1,9 @@ namespace Grains def grains (square : Int) : Option Nat := - sorry + sorry --remove this line and implement the function def totalGrains : Nat := - sorry + sorry --remove this line and implement the function end Grains diff --git a/exercises/practice/grep/Grep.lean b/exercises/practice/grep/Grep.lean index 82d8ba8..2f4d1f8 100644 --- a/exercises/practice/grep/Grep.lean +++ b/exercises/practice/grep/Grep.lean @@ -1,6 +1,6 @@ namespace Grep def grep (args : List String) : IO Unit := - sorry + sorry --remove this line and implement the function end Grep diff --git a/exercises/practice/hamming/Hamming.lean b/exercises/practice/hamming/Hamming.lean index fd7723f..6aaf063 100644 --- a/exercises/practice/hamming/Hamming.lean +++ b/exercises/practice/hamming/Hamming.lean @@ -1,6 +1,6 @@ namespace Hamming def distance (strand1 : String) (strand2 : String) : Option Nat := - sorry + sorry --remove this line and implement the function end Hamming diff --git a/exercises/practice/high-scores/HighScores.lean b/exercises/practice/high-scores/HighScores.lean index a2271e7..499aa12 100644 --- a/exercises/practice/high-scores/HighScores.lean +++ b/exercises/practice/high-scores/HighScores.lean @@ -1,21 +1,21 @@ namespace HighScores def latestList (scores : List Nat) : Nat := - sorry + sorry --remove this line and implement the function def latestArray (scores : Array Nat) : Nat := - sorry + sorry --remove this line and implement the function def personalBestList (scores : List Nat) : Nat := - sorry + sorry --remove this line and implement the function def personalBestArray (scores : Array Nat) : Nat := - sorry + sorry --remove this line and implement the function def personalTopThreeList (scores : List Nat) : List Nat := - sorry + sorry --remove this line and implement the function def personalTopThreeArray (scores : Array Nat) : Array Nat := - sorry + sorry --remove this line and implement the function end HighScores diff --git a/exercises/practice/house/House.lean b/exercises/practice/house/House.lean index c75b3c1..ccfc100 100644 --- a/exercises/practice/house/House.lean +++ b/exercises/practice/house/House.lean @@ -3,6 +3,6 @@ namespace House abbrev VerseIndex := { x : Nat // 1 ≤ x ∧ x ≤ 12 } def recite (startVerse endVerse : VerseIndex) : String := - sorry + sorry --remove this line and implement the function end House diff --git a/exercises/practice/isbn-verifier/IsbnVerifier.lean b/exercises/practice/isbn-verifier/IsbnVerifier.lean index 5e2bc1c..f9036c0 100644 --- a/exercises/practice/isbn-verifier/IsbnVerifier.lean +++ b/exercises/practice/isbn-verifier/IsbnVerifier.lean @@ -1,6 +1,6 @@ namespace IsbnVerifier def isValid (isbn : String) : Bool := - sorry + sorry --remove this line and implement the function end IsbnVerifier diff --git a/exercises/practice/isogram/Isogram.lean b/exercises/practice/isogram/Isogram.lean index 96da70c..1b9619e 100644 --- a/exercises/practice/isogram/Isogram.lean +++ b/exercises/practice/isogram/Isogram.lean @@ -1,6 +1,6 @@ namespace Isogram def isIsogram (phrase : String) : Bool := - sorry + sorry --remove this line and implement the function end Isogram diff --git a/exercises/practice/knapsack/Knapsack.lean b/exercises/practice/knapsack/Knapsack.lean index 6cc2172..b04948a 100644 --- a/exercises/practice/knapsack/Knapsack.lean +++ b/exercises/practice/knapsack/Knapsack.lean @@ -5,6 +5,6 @@ structure Item where value : Int def maximumValue (maximumWeight : Nat) (items : Array Item) : Int := - sorry + sorry --remove this line and implement the function end Knapsack diff --git a/exercises/practice/largest-series-product/LargestSeriesProduct.lean b/exercises/practice/largest-series-product/LargestSeriesProduct.lean index 9c42b6a..7a0a813 100644 --- a/exercises/practice/largest-series-product/LargestSeriesProduct.lean +++ b/exercises/practice/largest-series-product/LargestSeriesProduct.lean @@ -1,6 +1,6 @@ namespace LargestSeriesProduct def largestProduct (span : Nat) (digits : String) : Option Nat := - sorry + sorry --remove this line and implement the function end LargestSeriesProduct diff --git a/exercises/practice/leap/Leap.lean b/exercises/practice/leap/Leap.lean index 7318d8a..268cdbe 100644 --- a/exercises/practice/leap/Leap.lean +++ b/exercises/practice/leap/Leap.lean @@ -1,6 +1,6 @@ namespace Leap def leapYear (year : UInt16) : Bool := - sorry + sorry --remove this line and implement the function end Leap diff --git a/exercises/practice/line-up/LineUp.lean b/exercises/practice/line-up/LineUp.lean index a64bb44..6c59bb9 100644 --- a/exercises/practice/line-up/LineUp.lean +++ b/exercises/practice/line-up/LineUp.lean @@ -1,6 +1,6 @@ namespace LineUp def format (name : String) (number : Fin 1000) : String := - sorry + sorry --remove this line and implement the function end LineUp diff --git a/exercises/practice/linked-list/LinkedList.lean b/exercises/practice/linked-list/LinkedList.lean index 4592ead..b5e0a6f 100644 --- a/exercises/practice/linked-list/LinkedList.lean +++ b/exercises/practice/linked-list/LinkedList.lean @@ -6,24 +6,24 @@ structure LinkedList (σ α : Type) where -- You should define a data structure LinkedList to represent your doubly-linked list here. def LinkedList.empty : ST σ (LinkedList σ α) := - sorry + sorry --remove this line and implement the function def LinkedList.count (list : LinkedList σ α) : ST σ Nat := - sorry + sorry --remove this line and implement the function def LinkedList.push (value : α) (list : LinkedList σ α) : ST σ Unit := - sorry + sorry --remove this line and implement the function def LinkedList.unshift (value : α) (list : LinkedList σ α) : ST σ Unit := - sorry + sorry --remove this line and implement the function def LinkedList.pop (list : LinkedList σ α) : ST σ (Option α) := - sorry + sorry --remove this line and implement the function def LinkedList.shift (list : LinkedList σ α) : ST σ (Option α) := - sorry + sorry --remove this line and implement the function def LinkedList.delete (value : α) (list : LinkedList σ α) : ST σ Unit := - sorry + sorry --remove this line and implement the function end LinkedList diff --git a/exercises/practice/luhn/Luhn.lean b/exercises/practice/luhn/Luhn.lean index 417aa51..29d1806 100644 --- a/exercises/practice/luhn/Luhn.lean +++ b/exercises/practice/luhn/Luhn.lean @@ -1,6 +1,6 @@ namespace Luhn def valid (value : String) : Bool := - sorry + sorry --remove this line and implement the function end Luhn diff --git a/exercises/practice/matching-brackets/MatchingBrackets.lean b/exercises/practice/matching-brackets/MatchingBrackets.lean index 3a4df0f..c48fb18 100644 --- a/exercises/practice/matching-brackets/MatchingBrackets.lean +++ b/exercises/practice/matching-brackets/MatchingBrackets.lean @@ -1,6 +1,6 @@ namespace MatchingBrackets def isPaired (value : String) : Bool := - sorry + sorry --remove this line and implement the function end MatchingBrackets diff --git a/exercises/practice/matrix/Matrix.lean b/exercises/practice/matrix/Matrix.lean index bb94029..fc8e947 100644 --- a/exercises/practice/matrix/Matrix.lean +++ b/exercises/practice/matrix/Matrix.lean @@ -1,9 +1,9 @@ namespace Matrix def row (xs : String) (n : Nat) : List Nat := - sorry + sorry --remove this line and implement the function def column (xs : String) (n : Nat) : List Nat := - sorry + sorry --remove this line and implement the function end Matrix diff --git a/exercises/practice/meetup/Meetup.lean b/exercises/practice/meetup/Meetup.lean index 5e91ced..0e28b3b 100644 --- a/exercises/practice/meetup/Meetup.lean +++ b/exercises/practice/meetup/Meetup.lean @@ -22,6 +22,6 @@ inductive Week where deriving BEq, Repr def meetup (dayOfWeek : DayOfWeek) (month : Month) (week : Week) (year : Nat) : String := - sorry + sorry --remove this line and implement the function end Meetup diff --git a/exercises/practice/nth-prime/NthPrime.lean b/exercises/practice/nth-prime/NthPrime.lean index 6adf527..8822d99 100644 --- a/exercises/practice/nth-prime/NthPrime.lean +++ b/exercises/practice/nth-prime/NthPrime.lean @@ -1,6 +1,6 @@ namespace NthPrime def prime (n : Nat) : Option Nat := - sorry + sorry --remove this line and implement the function end NthPrime diff --git a/exercises/practice/palindrome-products/PalindromeProducts.lean b/exercises/practice/palindrome-products/PalindromeProducts.lean index 75d5c41..6e0bfd6 100644 --- a/exercises/practice/palindrome-products/PalindromeProducts.lean +++ b/exercises/practice/palindrome-products/PalindromeProducts.lean @@ -12,9 +12,9 @@ structure Result where deriving BEq, Repr def smallest (min max : Nat) (_ : min ≤ max) : Option Result := - sorry + sorry --remove this line and implement the function def largest (min max : Nat) (_ : min ≤ max) : Option Result := - sorry + sorry --remove this line and implement the function end PalindromeProducts diff --git a/exercises/practice/pangram/Pangram.lean b/exercises/practice/pangram/Pangram.lean index 94ef46d..db72a92 100644 --- a/exercises/practice/pangram/Pangram.lean +++ b/exercises/practice/pangram/Pangram.lean @@ -1,6 +1,6 @@ namespace Pangram def isPangram (sentence : String) : Bool := - sorry + sorry --remove this line and implement the function end Pangram diff --git a/exercises/practice/parallel-letter-frequency/ParallelLetterFrequency.lean b/exercises/practice/parallel-letter-frequency/ParallelLetterFrequency.lean index 008858b..707a2dd 100644 --- a/exercises/practice/parallel-letter-frequency/ParallelLetterFrequency.lean +++ b/exercises/practice/parallel-letter-frequency/ParallelLetterFrequency.lean @@ -3,6 +3,6 @@ import Std namespace ParallelLetterFrequency def calculateFrequencies (texts : List String) : IO (Std.TreeMap Char Nat) := - sorry + sorry --remove this line and implement the function end ParallelLetterFrequency diff --git a/exercises/practice/perfect-numbers/PerfectNumbers.lean b/exercises/practice/perfect-numbers/PerfectNumbers.lean index 6d3b964..ef1b659 100644 --- a/exercises/practice/perfect-numbers/PerfectNumbers.lean +++ b/exercises/practice/perfect-numbers/PerfectNumbers.lean @@ -7,6 +7,6 @@ def Positive := { x : Nat // x > 0 } -/ def classify (number : Positive) : Classification := - sorry + sorry --remove this line and implement the function end PerfectNumbers diff --git a/exercises/practice/phone-number/PhoneNumber.lean b/exercises/practice/phone-number/PhoneNumber.lean index f9e1470..de65e7a 100644 --- a/exercises/practice/phone-number/PhoneNumber.lean +++ b/exercises/practice/phone-number/PhoneNumber.lean @@ -1,6 +1,6 @@ namespace PhoneNumber def clean (phrase : String) : Option String := - sorry + sorry --remove this line and implement the function end PhoneNumber diff --git a/exercises/practice/prime-factors/PrimeFactors.lean b/exercises/practice/prime-factors/PrimeFactors.lean index f319598..e18861f 100644 --- a/exercises/practice/prime-factors/PrimeFactors.lean +++ b/exercises/practice/prime-factors/PrimeFactors.lean @@ -1,6 +1,6 @@ namespace PrimeFactors def factors (value : Nat) : List Nat := - sorry + sorry --remove this line and implement the function end PrimeFactors diff --git a/exercises/practice/protein-translation/ProteinTranslation.lean b/exercises/practice/protein-translation/ProteinTranslation.lean index 71b3ace..00c4933 100644 --- a/exercises/practice/protein-translation/ProteinTranslation.lean +++ b/exercises/practice/protein-translation/ProteinTranslation.lean @@ -11,6 +11,6 @@ inductive Protein where deriving BEq, Repr def proteins (strand : String) : Except String (Array Protein) := - sorry + sorry --remove this line and implement the function end ProteinTranslation diff --git a/exercises/practice/pythagorean-triplet/PythagoreanTriplet.lean b/exercises/practice/pythagorean-triplet/PythagoreanTriplet.lean index a015101..fe7bd93 100644 --- a/exercises/practice/pythagorean-triplet/PythagoreanTriplet.lean +++ b/exercises/practice/pythagorean-triplet/PythagoreanTriplet.lean @@ -1,6 +1,6 @@ namespace PythagoreanTriplet def tripletsWithSum (sum : Nat) : List (List Nat) := - sorry - + sorry --remove this line and implement the function + end PythagoreanTriplet diff --git a/exercises/practice/rail-fence-cipher/RailFenceCipher.lean b/exercises/practice/rail-fence-cipher/RailFenceCipher.lean index 59a9e8f..4a4e1ce 100644 --- a/exercises/practice/rail-fence-cipher/RailFenceCipher.lean +++ b/exercises/practice/rail-fence-cipher/RailFenceCipher.lean @@ -3,9 +3,9 @@ namespace RailFenceCipher def Positive := { x : Nat // x > 0 } def encode (rails : Positive) (msg : String) : String := - sorry + sorry --remove this line and implement the function def decode (rails : Positive) (msg : String) : String := - sorry + sorry --remove this line and implement the function end RailFenceCipher diff --git a/exercises/practice/raindrops/Raindrops.lean b/exercises/practice/raindrops/Raindrops.lean index b56ded3..335f295 100644 --- a/exercises/practice/raindrops/Raindrops.lean +++ b/exercises/practice/raindrops/Raindrops.lean @@ -1,6 +1,6 @@ namespace Raindrops def convert (number : Nat) : String := - sorry + sorry --remove this line and implement the function end Raindrops diff --git a/exercises/practice/rational-numbers/RationalNumbers.lean b/exercises/practice/rational-numbers/RationalNumbers.lean index 1d00cf7..5dd90f8 100644 --- a/exercises/practice/rational-numbers/RationalNumbers.lean +++ b/exercises/practice/rational-numbers/RationalNumbers.lean @@ -11,24 +11,24 @@ structure RationalNumber where deriving BEq, Repr def add (r1 r2 : RationalNumber) : RationalNumber := - sorry + sorry --remove this line and implement the function def sub (r1 r2 : RationalNumber) : RationalNumber := - sorry + sorry --remove this line and implement the function def mul (r1 r2 : RationalNumber) : RationalNumber := - sorry + sorry --remove this line and implement the function def div (r1 r2 : RationalNumber) : RationalNumber := - sorry + sorry --remove this line and implement the function def abs (r : RationalNumber) : RationalNumber := - sorry + sorry --remove this line and implement the function def exprational (r : RationalNumber) (n : Int) : RationalNumber := - sorry + sorry --remove this line and implement the function def expreal (x : Int) (r : RationalNumber) : Float := - sorry + sorry --remove this line and implement the function end RationalNumbers diff --git a/exercises/practice/rectangles/Rectangles.lean b/exercises/practice/rectangles/Rectangles.lean index ed5e188..80d567e 100644 --- a/exercises/practice/rectangles/Rectangles.lean +++ b/exercises/practice/rectangles/Rectangles.lean @@ -1,6 +1,6 @@ namespace Rectangles def rectangles (strings : Array String) : Nat := - sorry + sorry --remove this line and implement the function end Rectangles diff --git a/exercises/practice/relative-distance/RelativeDistance.lean b/exercises/practice/relative-distance/RelativeDistance.lean index 5341dc7..a8666f7 100644 --- a/exercises/practice/relative-distance/RelativeDistance.lean +++ b/exercises/practice/relative-distance/RelativeDistance.lean @@ -4,6 +4,6 @@ abbrev Parent := String abbrev Children := List String def degreeOfSeparation (familyTree : List (Parent × Children)) (personA : String) (personB : String) : Option Nat := - sorry + sorry --remove this line and implement the function end RelativeDistance diff --git a/exercises/practice/reverse-string/ReverseString.lean b/exercises/practice/reverse-string/ReverseString.lean index 5a4a27f..a7b3639 100644 --- a/exercises/practice/reverse-string/ReverseString.lean +++ b/exercises/practice/reverse-string/ReverseString.lean @@ -1,6 +1,6 @@ namespace ReverseString def reverse (value : String) : String := - sorry + sorry --remove this line and implement the function end ReverseString diff --git a/exercises/practice/rna-transcription/RnaTranscription.lean b/exercises/practice/rna-transcription/RnaTranscription.lean index 15e0274..f4d86cd 100644 --- a/exercises/practice/rna-transcription/RnaTranscription.lean +++ b/exercises/practice/rna-transcription/RnaTranscription.lean @@ -1,6 +1,6 @@ namespace RnaTranscription def toRna (dna : String) : String := - sorry + sorry --remove this line and implement the function end RnaTranscription diff --git a/exercises/practice/roman-numerals/RomanNumerals.lean b/exercises/practice/roman-numerals/RomanNumerals.lean index 5418f62..2eb1a5f 100644 --- a/exercises/practice/roman-numerals/RomanNumerals.lean +++ b/exercises/practice/roman-numerals/RomanNumerals.lean @@ -1,6 +1,6 @@ namespace RomanNumerals def roman (number : Fin 4000) : String := - sorry + sorry --remove this line and implement the function end RomanNumerals diff --git a/exercises/practice/rotational-cipher/RotationalCipher.lean b/exercises/practice/rotational-cipher/RotationalCipher.lean index 39de5d4..4d67d21 100644 --- a/exercises/practice/rotational-cipher/RotationalCipher.lean +++ b/exercises/practice/rotational-cipher/RotationalCipher.lean @@ -1,6 +1,6 @@ namespace RotationalCipher def rotate (shiftKey : UInt32) (text : String) : String := - sorry + sorry --remove this line and implement the function end RotationalCipher diff --git a/exercises/practice/run-length-encoding/RunLengthEncoding.lean b/exercises/practice/run-length-encoding/RunLengthEncoding.lean index 60df57d..6b17e7c 100644 --- a/exercises/practice/run-length-encoding/RunLengthEncoding.lean +++ b/exercises/practice/run-length-encoding/RunLengthEncoding.lean @@ -1,9 +1,9 @@ namespace RunLengthEncoding def encode (string : String) : String := - sorry + sorry --remove this line and implement the function def decode (string : String) : String := - sorry + sorry --remove this line and implement the function end RunLengthEncoding diff --git a/exercises/practice/satellite/Satellite.lean b/exercises/practice/satellite/Satellite.lean index 9c21380..d19b339 100644 --- a/exercises/practice/satellite/Satellite.lean +++ b/exercises/practice/satellite/Satellite.lean @@ -11,6 +11,6 @@ inductive Result where deriving BEq, Repr def treeFromTraversals (preorder inorder : List Char) : Result := - sorry + sorry --remove this line and implement the function end Satellite diff --git a/exercises/practice/say/Say.lean b/exercises/practice/say/Say.lean index 2ee60b5..07d1a7f 100644 --- a/exercises/practice/say/Say.lean +++ b/exercises/practice/say/Say.lean @@ -1,6 +1,6 @@ namespace Say def say (number : Fin 1000000000000) : String := - sorry + sorry --remove this line and implement the function end Say diff --git a/exercises/practice/scrabble-score/ScrabbleScore.lean b/exercises/practice/scrabble-score/ScrabbleScore.lean index 5ee2c6f..e94ec13 100644 --- a/exercises/practice/scrabble-score/ScrabbleScore.lean +++ b/exercises/practice/scrabble-score/ScrabbleScore.lean @@ -1,6 +1,6 @@ namespace ScrabbleScore def score (word : String) : Int := - sorry + sorry --remove this line and implement the function end ScrabbleScore diff --git a/exercises/practice/secret-handshake/SecretHandshake.lean b/exercises/practice/secret-handshake/SecretHandshake.lean index c7b553b..7bb8eb5 100644 --- a/exercises/practice/secret-handshake/SecretHandshake.lean +++ b/exercises/practice/secret-handshake/SecretHandshake.lean @@ -8,6 +8,6 @@ inductive Action where deriving BEq, Repr def commands (number : BitVec 5) : Array Action := - sorry + sorry --remove this line and implement the function end SecretHandshake diff --git a/exercises/practice/series/Series.lean b/exercises/practice/series/Series.lean index 014e18d..23b6080 100644 --- a/exercises/practice/series/Series.lean +++ b/exercises/practice/series/Series.lean @@ -1,6 +1,6 @@ namespace Series def slices (series : String) (sliceLength : Nat) : Option (Array String) := - sorry + sorry --remove this line and implement the function end Series diff --git a/exercises/practice/sgf-parsing/SgfParsing.lean b/exercises/practice/sgf-parsing/SgfParsing.lean index 13d1ee7..88c69c3 100644 --- a/exercises/practice/sgf-parsing/SgfParsing.lean +++ b/exercises/practice/sgf-parsing/SgfParsing.lean @@ -8,6 +8,6 @@ structure SgfTree where deriving Repr def parse (encoded : String) : Except String SgfTree := - sorry + sorry --remove this line and implement the function end SgfParsing diff --git a/exercises/practice/space-age/SpaceAge.lean b/exercises/practice/space-age/SpaceAge.lean index 42ed0ee..2a2edff 100644 --- a/exercises/practice/space-age/SpaceAge.lean +++ b/exercises/practice/space-age/SpaceAge.lean @@ -1,6 +1,6 @@ namespace SpaceAge def age (planet : Planet) (seconds : Nat) : Float := - sorry + sorry --remove this line and implement the function end SpaceAge diff --git a/exercises/practice/square-root/SquareRoot.lean b/exercises/practice/square-root/SquareRoot.lean index ae13242..20c05d6 100644 --- a/exercises/practice/square-root/SquareRoot.lean +++ b/exercises/practice/square-root/SquareRoot.lean @@ -1,6 +1,6 @@ namespace SquareRoot def squareRoot (radicand : Nat) : Nat := - sorry + sorry --remove this line and implement the function end SquareRoot diff --git a/exercises/practice/sublist/Sublist.lean b/exercises/practice/sublist/Sublist.lean index 7580dbc..a62f3ce 100644 --- a/exercises/practice/sublist/Sublist.lean +++ b/exercises/practice/sublist/Sublist.lean @@ -5,6 +5,6 @@ inductive Classification where deriving BEq, Repr def sublist (listOne listTwo : List Nat) : Classification := - sorry + sorry --remove this line and implement the function end Sublist diff --git a/exercises/practice/sum-of-multiples/SumOfMultiples.lean b/exercises/practice/sum-of-multiples/SumOfMultiples.lean index fb3039d..f0da2f8 100644 --- a/exercises/practice/sum-of-multiples/SumOfMultiples.lean +++ b/exercises/practice/sum-of-multiples/SumOfMultiples.lean @@ -1,6 +1,6 @@ namespace SumOfMultiples def sum (factors : List UInt64) (limit : UInt64) : UInt64 := - sorry + sorry --remove this line and implement the function end SumOfMultiples diff --git a/exercises/practice/transpose/Transpose.lean b/exercises/practice/transpose/Transpose.lean index 761879a..68a9b1b 100644 --- a/exercises/practice/transpose/Transpose.lean +++ b/exercises/practice/transpose/Transpose.lean @@ -1,6 +1,6 @@ namespace Transpose def transpose (lines : String) : String := - sorry + sorry --remove this line and implement the function end Transpose diff --git a/exercises/practice/triangle/Triangle.lean b/exercises/practice/triangle/Triangle.lean index 920843a..255b58b 100644 --- a/exercises/practice/triangle/Triangle.lean +++ b/exercises/practice/triangle/Triangle.lean @@ -1,12 +1,12 @@ namespace Triangle def equilateral (sides : List Float) : Bool = - sorry + sorry --remove this line and implement the function def isosceles (sides : List Float) : Bool = - sorry + sorry --remove this line and implement the function def scalene (sides : List Float) : Bool = - sorry + sorry --remove this line and implement the function end Triangle diff --git a/exercises/practice/twelve-days/TwelveDays.lean b/exercises/practice/twelve-days/TwelveDays.lean index e38218d..5e06fa0 100644 --- a/exercises/practice/twelve-days/TwelveDays.lean +++ b/exercises/practice/twelve-days/TwelveDays.lean @@ -3,6 +3,6 @@ namespace TwelveDays abbrev VerseIndex := { x : Nat // 1 ≤ x ∧ x ≤ 12 } def recite (startVerse endVerse : VerseIndex) : List String := - sorry + sorry --remove this line and implement the function end TwelveDays diff --git a/exercises/practice/two-bucket/TwoBucket.lean b/exercises/practice/two-bucket/TwoBucket.lean index 8384f20..3c4c7f2 100644 --- a/exercises/practice/two-bucket/TwoBucket.lean +++ b/exercises/practice/two-bucket/TwoBucket.lean @@ -14,6 +14,6 @@ structure Result where deriving BEq, Repr def measure (first second : Capacity) (goal : Volume) (start : BucketId) : Option Result := - sorry + sorry --remove this line and implement the function end TwoBucket diff --git a/exercises/practice/two-fer/TwoFer.lean b/exercises/practice/two-fer/TwoFer.lean index 4753182..0bd59d8 100644 --- a/exercises/practice/two-fer/TwoFer.lean +++ b/exercises/practice/two-fer/TwoFer.lean @@ -1,6 +1,6 @@ namespace TwoFer def twoFer (name : Option String) : String := - sorry + sorry --remove this line and implement the function end TwoFer diff --git a/exercises/practice/word-count/WordCount.lean b/exercises/practice/word-count/WordCount.lean index d78327a..1024b44 100644 --- a/exercises/practice/word-count/WordCount.lean +++ b/exercises/practice/word-count/WordCount.lean @@ -3,6 +3,6 @@ import Std namespace WordCount def countWords : String -> Std.HashMap String Nat := - sorry + sorry --remove this line and implement the function end WordCount diff --git a/exercises/practice/wordy/Wordy.lean b/exercises/practice/wordy/Wordy.lean index b785645..4e20f92 100644 --- a/exercises/practice/wordy/Wordy.lean +++ b/exercises/practice/wordy/Wordy.lean @@ -1,6 +1,6 @@ namespace Wordy def answer (question : String) : Option Int := - sorry + sorry --remove this line and implement the function end Wordy diff --git a/exercises/practice/yacht/Yacht.lean b/exercises/practice/yacht/Yacht.lean index f273c55..10cd105 100644 --- a/exercises/practice/yacht/Yacht.lean +++ b/exercises/practice/yacht/Yacht.lean @@ -10,6 +10,6 @@ abbrev Die := { x : Nat // 1 ≤ x ∧ x ≤ 6 } abbrev Throw := Vector Die 5 def score (dice : Throw) (category: Category) : Nat := - sorry + sorry --remove this line and implement the function end Yacht diff --git a/exercises/practice/zebra-puzzle/ZebraPuzzle.lean b/exercises/practice/zebra-puzzle/ZebraPuzzle.lean index 03cd4dc..95fb60c 100644 --- a/exercises/practice/zebra-puzzle/ZebraPuzzle.lean +++ b/exercises/practice/zebra-puzzle/ZebraPuzzle.lean @@ -9,9 +9,9 @@ inductive Nationality where deriving BEq, Inhabited, Repr def drinksWater : Nationality := - sorry + sorry --remove this line and implement the function def ownsZebra : Nationality := - sorry + sorry --remove this line and implement the function end ZebraPuzzle