Programming paradigms that change how people think about coding (2014)(ybrikman.com)

  (defmacro lay [[sym expr & more-bindings] & body]
    (let [delay-sym (gensym (str "laid-" sym "-"))]
      `(let [~delay-sym (delay ~expr)]
         (symbol-macrolet [~sym (deref ~delay-sym)]
           ~@(if (empty? more-bindings)
               body
               `[(lay ~more-bindings ~@body)])))))

    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 (prf) if x < y is True
        Yes prf => print (add x y prf)  -- yes, we got a prf, pass it to add
        No => putStrLn "no prf, x is not less than y"  -- the prf variable is not available in this case

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