Subject: FormalContent

Keywords: ::Refiner

Title: Goals and Sequents

--------------------------------------------------

<goal> : <sequent> # <annotations>
<sequent> : <assumption> list # <conclusion>
<assumption> : <hidden> # <id> # <type> 

As a term:
<goal> > !nf_goal(<sequent>; <term> !annotation_cons ilist) 
<sequent> : <term>
          | !inf_sequent{<hidden>:b}(<term>; <var>.<sequent>)


Assumptions are called by various names such as assum, declaration,  
decl, hypothesis, and most commonly hyp.

Sequent is what the rules see.
Goal is what the tactics see.
⋅
--------------------------------------------------

Authors: 

Contributors: RICH:t

⋅

Home