%foreign "C:getchar,libc 6"
%extern

%foreign "scheme,chez:get-char (current-input-port)"

%foreign "C:idris2_getStr, libidris2_support, idris_support.h"
%extern
prim__getStr : PrimIO String

%foreign "scheme,chez:get-line (current-input-port)"
prim__getLine : PrimIO String

%foreign "C:putchar,libc 6"
%extern

%foreign "scheme,chez:put-char (current-output-port)"

%foreign "C:idris2_putStr, libidris2_support, idris_support.h"
%extern
prim__putStr : String -> PrimIO ()

%foreign "scheme,chez:put-string (current-output-port)"
prim__putString : String -> PrimIO ()

  getLine = MkIO prim__getStr

  getLine = MkIO prim__getLine

  putString s = MkIO $ prim__putStr s

  putString s = MkIO $ prim__putString s

-- Unit

  MkPair : {a, b : Type} -> (x : a) -> (y : b) -> Pair a b

  MkPair : (x : a) -> (y : b) -> Pair a b

the : (0 t : Type) -> (a : t) -> t
the _ x = x

the : (0 t : Type) -> t -> t
the _ = identity

const : (x : a) -> ((0 _ : b) -> a)
const x = \_ => x

constant : a -> b -> a
constant x _ = x

flip : (f : a -> b -> c) -> b -> a -> c

flip : (a -> b -> c) -> b -> a -> c

(.) f g = \x => f (g x)

(.) f g x = f $ g x

  Yes : (prf : p)     -> Dec p
  No  : (ctr : Not p) -> Dec p

  Yes :     p -> Dec p
  No  : Not p -> Dec p

public export %inline
replace : forall x, y, p . (0 rule : x = y) -> p x -> p y
replace Refl prf = prf