35 lines
1.1 KiB
Idris
35 lines
1.1 KiB
Idris
module HomeworkTen
|
|
%default total
|
|
|
|
data Less : Nat -> Nat -> Type where
|
|
Suc : Less n (S n)
|
|
Trans : Less k n -> Less n m -> Less k m
|
|
|
|
data Sorted : List Nat -> Type where
|
|
SortedEmpty : Sorted []
|
|
SortedSingle : Sorted [x]
|
|
SortedCons : Less x y -> Sorted (y::tail) -> Sorted (x::y::tail)
|
|
|
|
threeLessThanFive : Less 3 5
|
|
threeLessThanFive = Trans Suc Suc
|
|
|
|
threeFiveSorted : Sorted [3,5]
|
|
threeFiveSorted = SortedCons threeLessThanFive SortedSingle
|
|
|
|
tailSorted : Sorted (x::xs) -> Sorted xs
|
|
tailSorted SortedEmpty impossible
|
|
tailSorted SortedSingle = SortedEmpty
|
|
tailSorted (SortedCons _ st) = st
|
|
|
|
firstSecondLess : Sorted (x::y::xs) -> Less x y
|
|
firstSecondLess SortedEmpty impossible
|
|
firstSecondLess SortedSingle impossible
|
|
firstSecondLess (SortedCons l _) = l
|
|
|
|
removeSecondSorted : Sorted (x::y::xs) -> Sorted (x::xs)
|
|
removeSecondSorted SortedEmpty impossible
|
|
removeSecondSorted SortedSingle impossible
|
|
removeSecondSorted (SortedCons _ SortedEmpty) impossible
|
|
removeSecondSorted (SortedCons _ SortedSingle) = SortedSingle
|
|
removeSecondSorted (SortedCons lxy (SortedCons lyr t)) = SortedCons (Trans lxy lyr) t
|