Dafny – A programming language with a program verifier

Re:Dafny – A programming language with a program verifier by pdw on Friday January 20, 2017 @08:06AM (#13443486)

I can't read MACLISP, but these two Common Lisp macros match the behavior that's described in the big comment:

    (defmacro defsmac (name params expr)
      `(defmacro ,name ,params
         (sublis (mapcar 'cons ',params (list ,@params)) ',expr)))
    
    (defmacro defmac (name params expr)
      `(defmacro ,name ,params
         (list '(lambda ,params ,expr) ,@params)))

[ Parent | on HN ]

Re:Dafny – A programming language with a program verifier by Animats on Friday January 20, 2017 @04:02PM (#13446948)

Thanks very much. It turns out the first one can be called with multiple args in the "expr" slot, so it has to be

    (defmacro defsmac (name params &rest expr)
      `(defmacro ,name ,params
         `,(cons 'progn (sublis (mapcar 'cons ',params 
                (list ,@params)) ', expr))))

but your code got me un-stuck.

[ Parent | on HN ]