fact: Definition Microbenchmarks_Env : Env Microbenchmarks_Carrier := (GLabelMap.empty (FuncSpec _)) ### ("std", "rand") ->> (Axiomatic FAny) ### ("list[W]", "nil") ->> (Axiomatic (FacadeImplementationOfConstructor (list W) nil)) ### ("list[W]", "push") ->> (Axiomatic (FacadeImplementationOfMutation_SCA (list W) cons)) ### ("list[W]", "pop") ->> (Axiomatic (List_pop W)) ### ("list[W]", "delete") ->> (Axiomatic (FacadeImplementationOfDestructor (list W))) ### ("list[W]", "empty?") ->> (Axiomatic (List_empty W)) ### ("list[list[W]]", "nil") ->> (Axiomatic (FacadeImplementationOfConstructor (list (list W)) nil)) ### ("list[list[W]]", "push") ->> (Axiomatic (FacadeImplementationOfMutation_ADT (list W) (list (list W)) cons)) ### ("list[list[W]]", "pop") ->> (Axiomatic (List_pop (list W))) ### ("list[list[W]]", "delete") ->> (Axiomatic (FacadeImplementationOfDestructor (list (list W)))) ### ("list[list[W]]", "empty?") ->> (Axiomatic (List_empty (list W))).
imports: CertifiedExtraction.Core CertifiedExtraction.FacadeUtils CertifiedExtraction.StringMapUtils CertifiedExtraction.Extraction.Internal CertifiedExtraction.Extraction.Extraction CertifiedExtraction.Benchmarks.Any Coq.NArith.NArith Coq.Program.Basics