Stream: Beginner Questions

Topic: Code printing underscores

view this post on Zulip David Wang (Dec 05 2025 at 17:02):

Hello,

How do I make an underscore print when exporting code. Example:

datatype ('a) type1 = Const_123 'a

definition "f1 x = undefined"

definition "f2 x (y::int) = y + f1 x"

code_printing
  constant f1 ⇀ (SML) "(fn Const_123 x => x)"

export_code f2
  in Eval

This results in:

fun f2 x y = Arith.plus_int y ((fn Constx123 x => x));

I want it to be:

fun f2 x y = Arith.plus_int y ((fn Const_123 x => x) x);

Isabelle uses underscores for arguments when printing code.

view this post on Zulip Mathias Fleury (Dec 06 2025 at 07:50):

Like pretty-much every technical question like this: grep the Isabelle source code and look how it is done at other places

view this post on Zulip Mathias Fleury (Dec 06 2025 at 07:51):

$ grep -A5 -r code_printing *
...
src/HOL/Code_Numeral.thy-    (SML) "Bit'_Shifts.push"

Last updated: Dec 08 2025 at 08:34 UTC