here's a full code example: import Data.String -- takes two integers, and a proof that x < y, and yields an integer add : (x : Integer) ->

here's a full code example: 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.