Some example code from the Orange Combinator Meetup

Combinator2.idr

module Combinator2

%default total


data LTE : Ord a => a -> a -> Type where
  XLTY : Ord a => (x : a) -> (y : a) -> { auto x_lt_y : LT = x `compare` y } -> x `LTE` y
  XEQY : Ord a => (x : a) -> (y : a) -> { auto x_eq_y : EQ = x `compare` y } -> x `LTE` y

lteExample : Combinator2.LTE 0 1
lteExample = 0 `XLTY` 1


Uninhabited (Interfaces.GT = Interfaces.EQ) where
  uninhabited Refl impossible


Uninhabited (Interfaces.GT = Interfaces.LT) where
  uninhabited Refl impossible


lteIsNotGT : Ord a => {x, y : a} -> (x_lte_y : GT = x `compare` y) -> Not (x `LTE` y)
lteIsNotGT x_gt_y (XLTY x y {x_lt_y}) = uninhabited $ trans x_gt_y $ sym x_lt_y
lteIsNotGT x_gt_y (XEQY x y {x_eq_y}) = uninhabited $ trans x_gt_y $ sym x_eq_y


isLTE : Ord a => (x : a) -> (y : a) -> Dec (x `LTE` y)
isLTE x y with (x `compare` y) proof x_compare_y
  isLTE x y | LT = Yes $ XLTY x y
  isLTE x y | EQ = Yes $ XEQY x y
  isLTE x y | GT = No $ lteIsNotGT x_compare_y


data In : List a -> (x : a) -> Type where
  Here : In (x :: xs) x
  There : In xs x -> In (y :: xs) x


inExample : In [1, 2, 3, 4] 4
inExample = There $ There $ There Here


namespace All
  data All : ( prop : a -> Type ) -> List a -> Type where
    Nil : All _ []
    (::) :
        { prop : a -> Type } ->
        { x : a } ->
        (prf : prop x) ->
        All prop xs ->
        All prop $ x :: xs


  data Odd : Nat -> Type where
    One : Odd 1
    PlusTwo : Odd n -> Odd $ S $ S n


  allExample : All Odd [1, 3, 5]
  allExample = [One, PlusTwo One, PlusTwo $ PlusTwo One]


  dependentPairExample : (n : Nat ** Odd n)
  dependentPairExample = (7 ** PlusTwo $ PlusTwo $ PlusTwo One)


excludedMiddleNotWrong : Not (Not (Either a (Not a)))
excludedMiddleNotWrong = \p => p $ Right (\x => p $ Left x)


namespace Ascending
  data LTEFirst : List a -> a -> Type where
    NilLTE : LTEFirst [] x
    HeadLTE : Ord a => {x, y : a} -> { x_lte_y : LTE x y } -> LTEFirst (y :: xs) x


  data Ascending : List a -> Type where
    Nil : Ascending []
    (::) : ( lte_first : LTEFirst xs x ) -> Ascending xs -> Ascending (x :: xs)

  
  ascendingExample5 : Ascending [4, 5]
  ascendingExample5 = [HeadLTE {x_lte_y = XLTY 4 5}, NilLTE]


  ascendingExample3 : Ascending []
  ascendingExample3 = []


  ascendingExample4 : Ascending [4]
  ascendingExample4 = [NilLTE]