Get the current datestamp, like "November 17, 2010 10:25:33".
In the logic this function reads from the ACL2 oracle. In the
execution we use Common Lisp's
See also universal-time, which returns an integer representation of the current time.
(defun date-fn (state) (declare (xargs :stobjs (state))) (declare (xargs :guard t)) (let ((__function__ 'date)) (declare (ignorable __function__)) (b* ((- (raise "Raw Lisp definition not installed?")) ((mv err val state) (read-acl2-oracle state))) (if (and (not err) (stringp val)) (mv val state) (mv "Error reading date." state)))))
(defthm stringp-of-date.datestamp (b* (((mv ?datestamp acl2::?state) (date-fn state))) (stringp datestamp)) :rule-classes :type-prescription)
(defthm state-p1-of-date.state (implies (force (state-p1 state)) (b* (((mv ?datestamp acl2::?state) (date-fn state))) (state-p1 state))) :rule-classes :rewrite)