clayrat

import java.time.{Instant, ZoneId, ZonedDateTime}

import scala.language.postfixOps
import scala.concurrent.ExecutionContext.Implicits._
import scala.concurrent.duration._
import scala.concurrent.duration.MILLISECONDS

import cats.syntax.apply._
import cats.syntax.flatMap._
import cats.syntax.functor._

clayrat

import prelude
import basics.isotoequiv

def curry (A B C : type) : ((A × B) → C) → (A → B → C) = 
  λ f a b → f (a, b)

def uncurry (A B C : type) : (A → B → C) → ((A × B) → C) = 
  λ f (a, b) → f a b

def iso/curry (A B C : type) : iso (A → B → C) ((A × B) → C) = 

clayrat

import Data.Vect
import Data.Fin

%default total
%access public export

data Ty : Type where
    TyBool: Ty
    TyInt: Ty
    TyFun: Ty -> Ty -> Ty

clayrat

import Control.Isomorphism
import Data.Fin

%default total

nif : Fin n -> Fin n
nif          FZ    = last
nif {n=S n} (FS k) = weaken $ nif k 

nifWeaken : (x : Fin n) -> nif (weaken x) = FS (nif x)

clayrat

module SumSimplify

%default total

-- from https://gist.github.com/iitalics/e060f27a04bba797f8bd3aa0ac04b3a3

-- 1+..+n = n*(n+1)/2

sumUpTo : Nat -> Nat
sumUpTo  Z    = Z

clayrat

import Data.NEList -- from idris-tparsec

nelList : Iso (List a) (Maybe (NEList a))
nelList = MkIso fromList (maybe Nil NEList.toList) fromTo toFrom
  where 
  fromTo : (y : Maybe (NEList a)) -> fromList (maybe [] NEList.toList y) = y
  fromTo Nothing = Refl
  fromTo (Just (MkNEList h t)) = Refl

  toFrom : (x : List a) -> maybe [] NEList.toList (fromList x) = x

clayrat

module TotalGCD

%default total

minusLT : (a, b : Nat) -> LT (S b) a -> LT (a `minus` (S b)) a
minusLT Z     b     lt = absurd lt
minusLT (S a) Z     lt = LTESucc $ rewrite minusZeroRight a in lteRefl
minusLT (S a) (S b) lt = lteSuccRight $ minusLT a b (fromLteSucc lt) 

threeway : (a, b : Nat) -> Either (a=b) (Either (LT a b) (LT b a))

clayrat

module GenericNSOP

import Data.List.Quantifiers

%default total
%access public export

data K = Star | Arr K K

interpK : K -> Type

clayrat

module L.Sub

import Data.List.Elem
import Subset

%default total

data Ty = A
        | Imp Ty Ty | Prod Ty Ty
        | Sub Ty Ty | Sum  Ty Ty

clayrat

module Dual.SeqCalc.Contextual

import Data.List
import Data.List.Elem
import Data.List.Quantifiers
import All
import Subset

%default total