		Search-engine friendly clone of the ACL2 documentation.

Try-gl-concls

Find true conclusions using GL

Given a list of possible conclusions, try-gl-concls uses gl to return the ones that are true (if any). For example, in the following form, try-gl-concls tells us that (not (equal (+ a b) 3)) and (not (equal (+ a b) 4)) are the only conclusions that are true.

(try-gl-concls test
  :hyp (and (unsigned-byte-p 1 a) (unsigned-byte-p 1 b))
  :concls ((not (equal (+ a b) 0))
           (not (equal (+ a b) 1))
           (not (equal (+ a b) 2))
           (not (equal (+ a b) 3))
           (not (equal (+ a b) 4)))
  :g-bindings (gl::auto-bindings (:mix (:nat a 8) (:nat b 8))))