fact: Definition GenExports av (n n' : nat) {consSigs : Vector.t consSig n} {methSigs : Vector.t methSig n'} (adtSpec : DecoratedADT (BuildADTSig consSigs methSigs)) (adtImpl : DecoratedADT (BuildADTSig consSigs methSigs)) (consWrapper : (forall midx, CodWrapperT av (methCod (Vector.nth methSigs midx)))) (domWrapper : (forall midx, DomWrapperT av (methDom (Vector.nth methSigs midx)))) (AbsR : Core.Rep adtSpec -> Core.Rep adtImpl -> Prop) (RepInv : Core.Rep adtImpl -> Prop) {numRepArgs : nat} (f : Core.Rep adtImpl -> Vector.t (Value av) numRepArgs) (f' : Core.Rep adtImpl -> Core.Rep adtImpl -> Vector.t ((Value av) * option av) numRepArgs) (H : forall x x0, is_same_types (Vector.to_list (f x0)) (Vector.to_list (f x)) = true) (ValidImpl : refineADT adtSpec adtImpl) : StringMap.t (AxiomaticSpec av) := List.fold_left (fun acc el => StringMap.add (methID (Vector.nth methSigs el)) (GenAxiomaticSpecs AbsR RepInv (consWrapper el) (domWrapper el) (Methods adtSpec el) f f' H) acc) (BuildFinUpTo n') (StringMap.empty _).
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.ADT.Core Bedrock.Platform.Facade.DFModule Fiat.ADTNotation Bedrock.Platform.Facade.CompileUnit2 Fiat.Common.i3list Fiat.Common.ilist3 CertifiedExtraction.Core CertifiedExtraction.FacadeUtils CertifiedExtraction.StringMapUtils CertifiedExtraction.Extraction.Internal CertifiedExtraction.Extraction.Extraction