Changeset 2493 for src/RTLabs


Ignore:
Timestamp:
Nov 26, 2012, 6:00:09 PM (7 years ago)
Author:
mckinna
Message:

Change in cst_well_defd to fix previously broken defn of translate_cst.
Fix, eventually, is to reconcile 2 defns of member (basics/lists/list.ma of return type bool, common/AST.ma of return type Prop).
Should now ensure that compiler.ma builds without BJC's commenting out.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r2490 r2493  
    273273  ].
    274274
     275(* JHM/BJC 2012.11.26: TODO fix this use of bool_to_Prop/remove other defn of member *)
    275276definition cst_well_defd : ∀ty.list ident → constant ty → Prop ≝ λty,globals,cst.
    276277  match cst with
    277   [ Oaddrsymbol id _ ⇒ member id (eq_identifier ?) globals
     278  [ Oaddrsymbol id _ ⇒ bool_to_Prop (member ? (eq_identifier ?) id globals)
    278279  | _ ⇒ True
    279280  ].
     
    302303  ] (pi2 … cst_sig).
    303304  [ cases (split_into_bytes ??) #lst
    304     #EQ >EQ >prf whd in ⊢ (??%?); cases size %
    305   | @cst_prf
     305    #EQ >EQ >prf whd in ⊢ (??%?); cases size %.
     306  | @cst_prf (* previously failed to typecheck here, until change 2012.11.26 above *)
    306307  |*: >prf %
    307308  ]
Note: See TracChangeset for help on using the changeset viewer.