Noratrieb/idris-learning
1
0
Fork 0
mirror of https://github.com/Noratrieb/idris-learning.git synced 2026-01-15 21:45:01 +01:00
Code Issues Projects Releases Packages Wiki Activity Actions

fin

Browse source
This commit is contained in:
nora 2021-07-15 15:38:52 +02:00
parent 5a58f22743
commit 1e8d2d6188
2 changed files with 64 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

24
chapter4/Types.idr
View file

@ -114,3 +114,27 @@ maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe Nothing y = y
maxMaybe x Nothing = x
maxMaybe a@(Just x) b@(Just y) = if x > y then a else b
data PowerSource = Petrol | Pedal
data Vehicle : PowerSource -> Type where
Bicycle : Vehicle Pedal
Car : (fuel : Nat) -> Vehicle Petrol
Bus : (fuel : Nat) -> Vehicle Petrol
-- exercise
Unicycle : Vehicle Pedal
Motorcycle : (fuel : Nat) -> Vehicle Petrol
wheels : Vehicle power -> Nat
wheels Bicycle = 2
wheels (Car fuel) = 4
wheels (Bus fuel) = 4
wheels Unicycle = 1
wheels (Motorcycle fuel) = 2
refuel : Vehicle Petrol -> Vehicle Petrol
refuel (Car fuel) = Car 100
refuel (Bus fuel) = Bus 200
refuel (Motorcycle fuel) = Motorcycle 100
refuel Bicycle impossible
refuel Unicycle impossible