add-require-x-less-than-y.idr

import Data.String

                                                  -- takes two integers, and a proof that x < y, and yields an integer
add : 
  (x : Integer) -> 
  (y : Integer) -> 
  (prf : x < y = True) ->                         -- require a proof that that x < y
  Integer
add x y prf = x + y

main : IO ()
main = do
  sx <- getLine                                   -- read string from input
  sy <- getLine                                   -- read string from input
  let Just x = parseInteger sx                    -- assuming int parse is ok, else error
  let Just y = parseInteger sy                    -- assuming int parse is ok, else error
  case decEq (x < y) True of                      -- decEq constructs a proof if x < y is True
    Yes prf => print (add x y prf)
    No => putStrLn "no prf, x is not less than y"

-- lets say I mess up the sign of the comparison on the case line and write decEq (x > y) instead... then I'd get a type error

--     When checking argument prf to function Main.add:
--     Type mismatch between
--                 x > y = True (Type of prf)
--         and
--                 x < y = True (Expected type)

-- there's no way to construct the prf value artificially, or sneak in different parameters that are unrelated to the prf value.

-- it's either a compile error or it's valid.