Subject: Fragments

Keywords: ::tactic

Title: Fragment tactic structures

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


Fragments assign some level of semantic explication to tactic
arguments. 

Could leave explication in fragments but lose argument explication in
instances. This would leave explication (tactic description obid) of tactic.
This would facilitate modification of arguments while maintaining indirect
explication throught the tactic description. Maybe better to implement
transformation methods of tactic application instances to remove or recover
semantic explication on demand.


<tactic_ap> : name_ap{<tactic_desc>:o, <tactic_name>}(<tactic_arg> subterms)
<tactic_arg> : <accessor>(<carrier>)
<carrier> : <carrier_opid>{<carrier_desc>:o, <arg_value>:<carrier_type}()
          | <carrier_opid>{<carrier_desc>:o}(<arg_term>)

When evaluated in ML:
<accessor> : term -> <argument syntactic type>
<carrier> : term


⋅
--------------------------------------------------

Authors: 

Contributors: RICH:t

⋅

Home