fact: Definition Sharpen_w_Delegates (DelegateIDs : nat) (AbstractReps : Fin.t DelegateIDs -> Type) (pRepT : (Fin.t DelegateIDs -> Type) -> Type) (RepT := pRepT AbstractReps) {n n'} (consSigs : Vector.t consSig n) (methSigs : Vector.t methSig n') (consDefs : ilist (B := consDef (Rep := RepT)) consSigs) (methDefs : ilist (B := methDef (Rep := RepT)) methSigs) (numDelegateConstructors : Fin.t DelegateIDs -> nat) (DelegateConstructorSigs : forall (idx : Fin.t DelegateIDs), Vector.t consSig (numDelegateConstructors idx)) (numDelegateMethods : Fin.t DelegateIDs -> nat) (DelegateMethodSigs : forall (idx : Fin.t DelegateIDs), Vector.t methSig (numDelegateMethods idx)) (DelegateSigs := fun idx => BuildADTSig (DelegateConstructorSigs idx) (DelegateMethodSigs idx)) (DelegateConstructorSpecs : forall (idx : Fin.t DelegateIDs), ilist (B := consDef (Rep := AbstractReps idx)) (DelegateConstructorSigs idx)) (DelegateMethodSpecs : forall (idx : Fin.t DelegateIDs), ilist (B := methDef (Rep := AbstractReps idx)) (DelegateMethodSigs idx)) (DelegateSpecs := fun idx => BuildADT (DelegateConstructorSpecs idx) (DelegateMethodSpecs idx)) (pAbsR : forall (A B : Fin.t DelegateIDs -> Type), (forall idx, A idx -> B idx -> Prop) -> pRepT A -> pRepT B -> Prop) (cAbsR := fun DelegateReps' DelegateConsImpls' DelegateMethImpls' (DelegateImpls' := fun idx => {| Rep := DelegateReps' idx; Constructors := DelegateConsImpls' idx; Methods := DelegateMethImpls' idx |}) (ValidImpls' : forall idx : Fin.t DelegateIDs, refineADT (DelegateSpecs idx) (DelegateImpls' idx)) r_o r_n => pAbsR _ _ (fun idx => AbsR (ValidImpls' idx)) r_o r_n) cConstructors cMethods cConstructorsRefinesSpec cMethodsRefinesSpec (ConcreteReps : Fin.t DelegateIDs -> Type) (DelegateImpls : forall idx, ADT (DelegateSigs idx)) (ValidImpls : forall idx : Fin.t DelegateIDs, refineADT (DelegateSpecs idx) (DelegateImpls idx)) := @Notation_Friendly_refinedUnderDelegates RepT _ _ _ consSigs methSigs consDefs methDefs DelegateSigs pRepT cConstructors cMethods DelegateSpecs cAbsR cConstructorsRefinesSpec cMethodsRefinesSpec.
imports: Fiat.QueryStructure.Automation.MasterPlan Bedrock.Memory