search

latte-central / LaTTe

LaTTe : a Laboratory for Type Theory experiments (in clojure)
http://latte-central.github.io/LaTTe/
MIT License
256 stars 13 forks source link

Generic primitive-kind--to--string mapping #23

Closed Bost closed 5 years ago

Bost commented 5 years ago

BTW I find the distinct macros deflemma, defthm, defaxiom to be a code redundancy. Would you accept a future PR merging these macros into one? Something like:

(defmacro defprimitive [kind & args]
  ...)

(defmacro defthm [& args]
  `(defprimitive ::theorem ~@args))

(defmacro deflemma [& args]
  `(defprimitive ::lemma ~@args))

(defmacro defaxiom [& args]
  `(defprimitive ::axiom ~@args))
fredokun commented 5 years ago

Thanks, there's a lot of redundancy its a useful simplification... For the defprimitive form to remove this redundancy ... this would be nice however I would rather like a defstatement or even better define-mathematical-statement ... The long name would suggest the fact that it's not really for the "public" consumption (however it would not be hidden)... So I could (and should) do that but if you are motivated I will of course consider the PR (without guarantee of direct integration, testing is best done via compiling (i.e. lein certify and/or lein codox) all the available LaTTe libraries)...