Stream: Isabelle/ML

Topic: Info of primrec

Jonas Stahl (Nov 15 2023 at 15:50):

Hi,
there's the function Function.get_info, which gives me the info and therefore the terms of functions created by fun and function. Is there also a function to get the terms of a primrec function?

Dmitriy Traytel (Nov 15 2023 at 17:10):

There is nothing user-relevant stored for functions defined using primrec, but you can find the simp rules and constants in the Spec_Rules database. Try:

ML ‹Spec_Rules.get @{context}›
ML ‹Spec_Rules.retrieve @{context} @{term "replicate"}›

Jonas Stahl (Nov 15 2023 at 21:00):

Thank you!

Last updated: May 04 2024 at 16:18 UTC