Tutorial Ltac2 : Ltac2 for Ltac1 Users

Main contributors

• Thomas Lamiaux

Summary

Ltac2 is the successor of Ltac1, and is designed to replace Ltac1 as the standard tactic language for the Rocq proof assistant. This tutorial is meant to introduce Ltac2 for users that already are familiar with Ltac1. We mainly focus on the differences with Ltac1, and how to translate your existing Ltac1 knowledge into Ltac2 idioms.

Table of contents

• 1. Introduction
  • 1.1 A Brief History of Ltac1
  • 1.2 Design Flaws of Ltac1
  • 1.3 Ltac2
  • 1.4 Status of Ltac2
• 2. Using Ltac2 to Write Proofs
  • 2.1 Using Ltac2 in the Ltac1 Proof Mode
  • 2.2 Using the Ltac2 Proof Mode
• 3. Ltac2 Is a Proper Functional Programming Language
  • 3.1 Types and Type Inference
  • 3.2 Call-by-Value Semantics and Thunking
  • 3.3 Effects: Printf and References
  • 3.4 Exceptions
• 4. Ltac2 as a Meta-Programming Language for Rocq
  • 4.1 Foreign Function Interface
  • 4.2 Matching Terms and Goals
  • 4.3 Quoting and Unquoting
  • 4.4 Backtracking
  • 4.5 Notations
• 5. Small Case Study

Prerequisites

Needed:

• Familiarity with Ltac1 and basic Rocq proof writing.

Installation:

• Ltac2 and its standard library are available by default with Rocq.

1. Introduction

1.1 A Brief History of Ltac1

Ltac1 was introduced in 2000 (Coq 7.0) to enable users to write their own tactics by combining existing primitive tactics using an expressive set of combinators. For instance, users have been using Ltac1 to write variants of existing tactics or domain-specific automation tactics. Ltac1 was key in the success of Rocq, and of many formalization efforts as it enabled us to write proofs in a more incremental, efficient and more robust way than the state of the art of that time.

1.2 Design Flaws of Ltac1

Yet, Ltac1 was not planned for such advanced uses and suffered from design flaws. 1. At the time, there was no idea of what a good tactic language ought to be and Ltac1 was not designed following current PL conventions. 2. The development of Ltac1 was not carefully planned, and features have been added piecemeal over time by different contributors. Consequently, the language is far from well-designed, uniform, or well implemented, making improvements and every day use complicated. 3. Ltac1 tried to accommodate two contradictory features: for tactics to be both automagical and predictable. To do so, Ltac1 implements many dynamic decision procedures to facilitate writing tactics that work well for small examples but do not scale well. With experience, there are several well-known design flaws with Ltac1:

• **No type system.** Ltac1 is completely untyped. Any value can be passed to any function, and type errors are only caught at runtime, often with cryptic error messages. This makes writing large libraries and tactics and debugging very tedious.
• **No data structures.** Ltac1 has no lists, no records, and no algebraic types. All state must be threaded through the goal or through side channels.
• **Unclear Semantics.** It is hard to predict when a tactic will be evaluated, or whether a name refers to a Rocq term or an Ltac1 variable. This leads to subtle and hard-to-diagnose bugs.
• **Limited effects.** Ltac1 lacks support for many basic effects that are useful in a programming language like printing, or mutable references.
• **Implicit quoting.** The boundary between Gallina (Rocq terms) and Ltac1 meta-programs is not syntactically marked. Ltac1 uses dynamic scoping rules to resolve names, which are hard to understand and debug.
• **Poor FFI.** Functions from the Rocq codebase are imported all at once, as tactics without types and without any control over what is in scope.

1.3 Ltac2

Ltac2 is designed to be the replacement of Ltac1, and offers both a reliable and scalable tactic language for Rocq, while being as backward compatible as possible. Its core improvements over Ltac1 are:

• It is a proper typed functional programming language of the Hindley–Milner family, similarly to OCaml, with type inference, algebraic data types, and a clear call-by-value semantics.
• It has an explicitly typed Foreign Function Interface. This makes it easy to extend Ltac2 to expose and access primitives like unification, that were not accessible before, while providing better documentation for it. As a consequence, it is possible to do more in Ltac2 than in Ltac1. For instance, it is now possible to manipulate the goal state, and modify the set of goals under focus etc.
• Quoting and unquoting between Rocq terms (Gallina) and Ltac2 values is now explicit and syntactically marked. It no longer relies on a hard-to-predict dynamic decision procedure.
• Backtracking is modelled as streams of possibilities, with fine-grained primitives to manipulate it.

1.4 Status of Ltac2

Ltac2 is actively developed and included in every Rocq distribution. No extra package is needed. Ltac2 may still contain bugs or limitations, but it is already more reliable and expressive than Ltac1. Therefore, while Ltac1 is not going away anytime soon, we would like to strongly encourage users to use Ltac2 (or other alternatives) instead of Ltac1 for new projects and new automation code in existing projects. It comes with a standard Library that is meant to contain basic building blocks for creating complex tactics. The standard Library keeps evolving and may contain more exposed primitives in more recent versions of Rocq. See https://github.com/rocq-prover/rocq/tree/master/theories/Ltac2 for the master branch of Rocq. Most notably, Ltac2 still lacks notations for some of the basic tactics. For the moment, Ltac2 is not loaded by default with the Prelude. It needs to be imported with From Ltac2 Require Import Ltac2. Additional modules can be required or imported if needed.

2. Using Ltac2 to Write Proofs

Before discussing the Ltac2 language itself, let us consider the differences between Ltac1 and Ltac2 proof modes, and how to use one in the other.

2.1 Using Ltac2 in the Ltac1 Proof Mode

The main use for Ltac2 is to write predictable tactics. Yet, you do not need to port your whole development to Ltac2 to benefit from Ltac2. You can write new scripts in Ltac2 but call them in the usual Ltac1 proof mode. This lets you enjoy Ltac2's type safety and expressiveness while leaving all existing proofs untouched, and avoid dealing with differences between Ltac1 and Ltac2's proof mode. Consequently, a natural approach when migrating a large development is: 1. Write new scripts in Ltac2 or port existing Ltac1 ones to Ltac2. 2. Import them into Ltac1 via ltac2:(...). 3. Use them in existing proof scripts without further changes. Importing Ltac2 automatically sets the proof mode to Ltac2. You can decide to keep using Ltac1 proof mode by using Set Proof Mode "Classic". Conversely, Set Proof Mode "Ltac2" to use the Ltac2 proof mode. You can then write scripts in Ltac2, and call them in a Ltac1 proof using ltac2:() wrapper. As an example, let us leverage the printf function for Ltac2.

We can verify the Ltac2 function itself works in a Ltac2 proof:

To call it from a Ltac1 proof script, wrap it with ltac2:(...). The Ltac2 expression inside must have type unit:

Importantly, ltac2:(...) creates a scope boundary: the code inside is pure Ltac2, and Ltac1 variables are not in scope there. For instance, in a Ltac1 function my_intro (id : ident) := ltac2:(intro id), the id inside ltac2:(...) would be treated as the Ltac2 literal name id, not as the Ltac1 variable. The resulting tactic would always introduce a hypothesis named id regardless of what was passed. To pass Ltac1 values across this boundary, one uses the binder syntax ltac2:(x1 .. xn |- expr), which explicitly receives Ltac1 values as Ltac2 arguments and binds them under the names x1 .. xn in the Ltac2 scope. Inside the expression, x1 .. xn have type Ltac1.t and are converted to typed Ltac2 values using helpers such as Ltac1.to_constr and Ltac1.to_ident. The Ltac2 wrapper must then be defined as a let-in and applied, due to Ltac1's inner workings.

2.2 Using the Ltac2 Proof Mode

The first possibility is to use Ltac2 proof mode directly. It is very similar to Ltac1 outside of a few syntax changes. Most noticeably, the dispatching syntax has changed. In Ltac1, when a tactic creates more than one new goal, you can specify which tactic to apply with the syntax tac1; [tac21 | tac22]. Moreover, tac1; tac2; [tac31 | tac32] is parsed as (tac1; tac2); [tac31 | tac32].

In Ltac2, this is now written with the syntax tac1 > [tac21 | tac22] in order to avoid confusion between chaining tactics and dispatching. The latter is asymetric and does not compose opposite to ;. Moreover, tac1; tac2 > [tac31 | tac32] is now parsed as tac1; (tac2 > [tac31 | tac32]) as Ltac2 no longer automatically delays tactic execution. Consequently, if tac1 generates multiple goals, the dispatcher will attempt to apply the list tac31|tac32 to the subgoals generated by tac2 independently for each goal produced by tac1. This typically results in an "Incorrect number of goals" error. To achieve standard Ltac1 factoring, you must use parentheses to explicitly group the sequence: (tac1; tac2) > foo|bar.

Similarly, some tactic combinators now parse as if they were normal functions. Parentheses are now required around complex arguments, such as abstractions. The tacticals affected are: try, repeat, do, once, progress, time, abstract. For instance, try exact HP is now parsed as (try exact) HP: try receives exact as its sole argument, and HP is left dangling, causing an error. It is hence required to write try (exact HP). Respectively for the others.

However, a real issue with the Ltac2 proof mode is that some functions are imported but are currently missing notations to handle the quoting from Rocq to Ltac2. For instance, in Rocq 9.0, the function clearbody is exposed in the standard library as: [Ltac2 @ external clearbody : ident list → unit := "rocq-runtime.plugins.ltac2" "tac_clearbody"] However, is lacking a notation enabling us to directly write clearbody x y to clear the body of the local definitions x and y. You would have to write the quoting yourself clearbody [@x; @y].

In the meantime, there are two main workarounds not to write the quoting yourself. The first option is to define the missing notation locally. In this case, one should also consider contributing it upstream to the standard library. The underlying primitive lives in Std and expects an ident list, so a notation using the list1(ident) parser -- which parses one or more space-separated identifiers -- is sufficient. See the corresponding section for more information.

The second option is to call the tactic through the Ltac1 compatibility bridge using ltac1:(...). This is the simplest workaround when you only need the tactic occasionally and do not want to introduce a local notation, but it comes with the usual caveats of mixing Ltac1 and Ltac2 (no type checking, limited interoperability with Ltac2 values).

More generally, any Ltac1 tactic can be embedded into Ltac2 using ltac1:(...). The resulting Ltac2 expression has type unit and runs the Ltac1 tactic on the current goal. However, ltac1:(...) creates a scope boundary: the code inside is pure Ltac1, and Ltac2 variables are not in scope there. For instance, in a function my_intro (id : ident) := ltac1:(intro id), the id inside ltac1:(...) would be treated as the Ltac1 literal name id, not as the Ltac2 variable -- so the tactic would always introduce a hypothesis named id regardless of what was passed. To pass Ltac2 values across this boundary, one uses the binder syntax ltac1:(x1 .. xn |- tac), which explicitly receives Ltac2 values as Ltac1 arguments and binds them under the names x1 .. xn in the Ltac1 scope. The resulting expression has type Ltac1.t → .. → Ltac1.t → unit and must be applied to the Ltac2 values, converted to Ltac1.t using helpers such as Ltac1.of_constr and Ltac1.of_ident.

3. Ltac2 Is a Proper Functional Programming Language

Ltac1 is a non standard tactic language with no type system, opaque dynamically-typed values, and a non-standard evaluation strategy, making tactics fragile and hard to predict and debug. In contrast, Ltac2 is a proper programming language that belongs to the well-known class of ML languages: it is a call-by-value functional language with a Hindley–Milner type system. Expressions have static types that can be inferred, so ill-typed programs are rejected at compile time rather than at runtime. Moreover, evaluation is fully predictable thanks to call-by-value semantics. This makes Ltac2 tactics reliable and composable by design, as opposed to Ltac1.

3.1 Types and Type Inference

The most fundamental difference between Ltac1 and Ltac2 is that Ltac2 is a statically typed language with Hindley–Milner type system, similarly to OCaml. In Ltac1 there is no type system: values are opaque and type errors are only caught at runtime with cryptic messages. In Ltac2, every expression has a type, and ill-typed programs are rejected before they are run. Type annotations are optional -- the type checker infers them -- but can be written for documentation or disambiguation. For instance, if we define an alias for integer addition, Ltac2 will automatically figure out the type is `int -> int -> int`:

Ltac2 supports Hindley–Milner polymorphism, also called prenex polymorphism. In prenex polymorphism, type-variable quantifiers must appear at the outermost level of the type, never nested inside it. For instance, ∀ 'a, 'a → 'a is a valid polymorphic type: the quantifier is at the front, and the function works at any type 'a. It is the type of a function that takes an input of type 'a and returns a value of the same type. However, ∀ 'a, (∀ 'b, 'b → 'b) → 'a is not valid because 'b is quantified inside the type. Note that it is not the same as ∀ 'a 'b, ('b → 'b) → 'a.

Ltac2 provides the following primitive types:

• unit: the unit type, with its single value ().
• bool: Booleans, with values true and false.
• int: machine integers (63-bit on a 64-bit platform).
• string: character strings.
• ident: Rocq identifiers (names of hypotheses, variables, …).
• constr: type of Rocq terms in Ltac2.

Beyond the built-in types, you can define your own algebraic data types with Ltac2 Type. As in OCaml, constructor names must start with an **uppercase** letter (Some, None, S, O, …), while variable and function names **must** start with a **lowercase** letter. For instance, a type for arithmetic expressions can be defined by:

Functions can then be defined with the rec keyword for recursion, and match for pattern-matching similarly to OCaml. Constructors are then referred to without parentheses, like Add a b.

The standard library provides some of the usual polymorphic types like list and option, and a few basic functions for them.

option represents a possibly-absent value: Some x for presence and None for absence. Here is a function returning the head of a list as an option, with pattern matching on the constructors of the list type:

3.2 Call-by-Value Semantics and Thunking

Ltac1 has an unclear, hard-to-predict evaluation order. Ltac2 is strictly **call-by-value**: function arguments are fully evaluated before the function body is entered. This makes behavior predictable and intuitive, but it has one important consequence for passing tactics as arguments. If you pass a tactic t as an argument to a function, t is evaluated -- i.e. executed -- immediately, before the body of the function has a chance to decide whether to use it. To illustrate this, consider a function that ignores its argument and does nothing:

Passing fail to bad_ignore causes the whole call to fail, because fail is evaluated before bad_ignore is entered:

The fix is to **thunk** the argument: wrap the tactic in fun () ⇒ .... A thunk is only evaluated when applied to (), so the callee can decide when (or whether) to run it.

Writing fun () ⇒ ... at every call site is noisy. A Ltac2 Notation with the thunk(tactic) parser inserts thunks automatically, hiding this detail from callers. For simple abbreviations (no extra parsing), it suffices to declare a notation that applies the thunked function:

3.3 Effects: Printf and References

Compared to Ltac1, Ltac2 has proper effects, notably printing and references.

3.3.1 Printf

In Ltac1, idtac is the only way to print, and there is no mutable state. Ltac2 has a proper typed printf. printf takes a format string with typed specifiers:

• i : prints an int
• I : prints an ident
• s : prints a string
• m : prints a message
• t : prints a constr (a Rocq term)
• a : prints a value of any type using a custom formatter fun () x ⇒ ...
• A : same as a but the formatter takes no unit argument
• % : outputs a literal %
  This makes it much easier to inspect the proof state or debug automation than the idtac approach. For instance, here is a small tactic to print the type of a hypothesis. We will explain the exact syntax in the next section.

3.3.2 Mutable References

Ltac2 provides ML-style mutable reference cells of type 'a ref. A reference is a box holding a single mutable value of type 'a. References make it possible to accumulate state across tactic calls — something that pure functional code cannot express. The Ref module provides the following primitives:

• Ref.ref v: creates a fresh reference initialised to v.
• Ref.get r: returns the current value of r.
• Ref.set r v: replaces the value stored in r with v.
• Ref.update r f: applies f to the current value and stores the result.

For int ref specifically, Ref.incr r and Ref.decr r add or subtract 1. For example, here is a tactic that tracks how many hypotheses it clears:

Note that mutations to a reference are **not rolled back on backtracking**. If a branch modifies a reference and then fails, the modification persists. Keep this in mind when combining references with backtracking tactics.

3.4 Exceptions

Ltac2 has a built-in type exn for exceptions. Several exceptions are predefined in the standard library:

• Tactic_failure (msg : message option) -- the standard tactic failure, raised by most combinators and by fail.
• Out_of_bounds (msg : message option) -- index out of range (e.g. list access).
• Division_by_zero -- integer division by zero.
• Invalid_argument (msg : message option) -- a function received an argument it cannot handle.
• Match_failure -- an inexhaustive pattern match was not satisfied.

The exn type is open: you can add your own variants with the syntax Ltac2 Type exn ::= [myEx (type)].

The easiest method to build a value of type message is to use fprintf, which works exactly like printf except it returns a message value instead of printing it. There are two primitives to raise an exception, with different semantics: 1. Control.throw : exn → 'a -- raises a **non-backtrackable** exception. It cannot be caught by the backtracking combinators Control.plus or try. It is meant for programming errors or hard failures where retrying makes no sense (analogous to a panic).

2. Control.zero : exn → 'a -- raises a **backtrackable** exception. It signals that the current branch has no solution, which triggers backtracking: Control.plus will try the alternative branch, and try will silently recover. See the corresponding section for more information.

4. Ltac2 as a Meta-Programming Language for Rocq

4.1 Foreign Function Interface

In Ltac1, all interaction with the Rocq codebase happens through built-in tactics imported as a single opaque block -- no types, no control over what is in scope. Ltac2 has an explicit, typed Foreign Function Interface (FFI). Rocq API -- kernel or higher-level functions -- can be easily exposed. This enables easy access to APIs that were not accessible in Ltac1, making Ltac2 much more expressive. Many APIs are exposed in different modules in the standard library available at: https://github.com/rocq-prover/rocq/tree/master/theories/Ltac2 Most notable examples:

• Control: interact with the proof state (goal) and backtracking
• Constr: inspect, build, and compare Rocq terms
• Std: reduce terms, call unification, access the environment
• Fresh: to create fresh ident
• Unification: to call unification in a controlled way
• Constr.Unsafe: to access the raw kernel representation of terms

The full standard library is at: https://github.com/rocq-prover/rocq/tree/master/theories/Ltac2 For example, Constr.type retrieves the type of a term and Std.eval_hnf reduces it to head-normal form:

4.2 Matching Terms and Goals

Ltac1 provides lazymatch, match and multimatch for matching patterns and goals. This still exists in Ltac2 but has changed syntax to avoid confusion with the match for matching algebraic types. The new syntax is lazy_match!, match!, and multi_match!. Otherwise, they work as in Ltac1. Although it is common in Ltac1 to use uppercase variables for hypotheses, like H, keep in mind in Ltac2 you need to use **lowercase** ones.

Another difference with Ltac1 is that a pattern containing variable bindings must now be explicit, whereas it used to be optional and dynamically figured out if not specified. For instance, to match let var := ?expr in ?body, one must write let var := ?expr in @?body var.

4.3 Quoting and Unquoting

One of the main sources of confusion in Ltac1 is the implicit boundary between Gallina (the language of Rocq terms) and Ltac1 meta-programs. Ltac1 uses dynamic scoping rules to resolve names, leading to subtle bugs when a name is mistaken for a Rocq term instead of an Ltac1 variable, or vice versa. The goal was to ease users' lives, but in practice this does not scale well. To fix this, Ltac2 makes this boundary **explicit** through quoting and unquoting operators. For example, a tactic that splits a conjunction and closes both goals with I:

In Ltac2, every Rocq term must be explicitly **quoted** with ' which produces a Ltac2 term of type constr, and **unquoted** to recover a Rocq term using $. Note, for complex implementation reason $ can only be applied to variables. If we wanted to rewrite ltac1_close_conj in Ltac2, we would take variable t : constr as argument, as constr is the only type we can manipulate. Yet, to apply it to exact which expects an unquoted term, which gives us:

To be able to use it with a Rocq value, one then need to quote it to a constr. For instance, like the following.

The quoting can be done automatically using a notation, we refer to the following section for further explanations.

The same applies to Rocq identifiers, which can be created using @. In Ltac1, you could just write:

In Ltac2, hypothesis names have the dedicated type ident. Write @name to create an ident literal, then use Control.hyp to recover the corresponding constr:

4.4 Backtracking

Ltac1 controls backtracking through:

• match goal (backtracks into branches on failure, etc.),
• Combinators like first [tac1 | tac2 | ...]
• fail n (propagates failure n levels up through match branches)

Ltac2 has more fine-grained controls on backtracking. Matching and combinators are still available. However, fail n is no longer supported; it was a hack to deal with the lack of good primitives for backtracking. Instead, Ltac2 has fine-grained primitives to manipulate values as streams of possibilities and backtracking. Combinators like first can then be reimplemented using these primitives. Most users do not need these primitives, and the existing combinators are enough. We mention them briefly, and refer to the documentation for more details. The three primitives are:

• Control.zero : exn → 'a -- raises an exception and triggers backtracking. This is the primitive underlying Ltac2 fail.
• Control.plus : (unit → 'a) → (exn → 'a) → 'a -- stacks a backtracking choice: try the first thunk; on exception, try the handler. This is the primitive underlying tac1 + tac2, but it is finer since different decisions can be performed depending on the exception raised.
• Control.case : (unit → 'a) → ('a × (exn → 'a)) result -- inspects whether a tactic has at least one success.

4.5 Notations

Ltac2 supports two kinds of custom syntax via Ltac2 Notation. An **abbreviation** is a Ltac2 Notation with no argument clause; it simply expands to a fixed Ltac2 expression. It does not add a new rule to the Ltac2 grammar nor new keywords: the name is resolved as a plain identifier at parse time, so it cannot cause parsing conflicts, e.g. with variable names. It should be used when you want a short name for a combinator or a fixed tactic sequence. In Rocq 9.2 or above, use Ltac2 Abbreviation.

A full Ltac2 Notation declares new parsing rules and keywords which are specified with "tac_name". Arguments are then given with the syntax name_arg(X) and X specifies that type of name_arg. The available argument parsers include: The basic atoms are:

• tactic / tactic(n) -- parse a tactic at precedence level n (default 5); evaluated eagerly, so use thunk when the argument is a tactic branch that must be delayed.
• thunk(e) -- parse e, then wrap the result in fun () ⇒ .... The most common form is thunk(tactic), which turns each tactic argument into a unit → unit thunk to prevent premature evaluation.
• ident -- parse a plain identifier (type ident).
• constr -- parse a Rocq term (type constr).
• string -- parse a string literal (type string).
• int -- parse an integer literal (type int).

There also are combinators for optional arguments and list of arguments:

• list0(e) -- parse a whitespace-separated, possibly empty, list of e
• list0(e, "sep") -- same, but with a literal keyword separator sep.
• list1(e) / list1(e, "sep") -- like list0 but require at least one element. The notation my_first [...] below uses list1(thunk(tactic(6)), "|") to parse one or more |-separated tactic branches.
• opt(e) -- parse an optional argument e of type option e
• seq(e1, e2, ...) -- parse a fixed sequence of entries and bind them as a tuple.

As an example consider reimplementing first using the backtracking operators as implemented in the Ltac2 standard library.

To write a notation for it, we write:

• "my_first" and "" / "" are literal keywords that the parser matches verbatim; so that my_first [...] is unambiguous
• tacs is the name bound in the body to the parsed argument
• list1(..., "|") parses a non-empty list of elements separated by |.
• tactic(6) parses one tactic branch at precedence level 6. Level 6 is high enough to accept most compound tactics, yet low enough that the parser stops at | and ""] instead of consuming them.
• thunk(...) wraps the parsed branch in fun () ⇒ ..., so each branch is turned into a thunk unit → unit. Without thunk, every branch would be executed eagerly -- before my_first0 even runs -- which would defeat the whole purpose of trying alternatives one by one.

The result is that my_first [t1 | t2 | t3] is elaborated to my_first0 [(fun () ⇒ t1); (fun () ⇒ t2); (fun () ⇒ t3)]. All together, it gives us the notation:

5. Small Case Study

Let us now consider a small case study and write a tactic simplify_let that takes a hypothesis h whose type is a let-in let var := expr in body[var], and turns it into body[x'], where x' := expr is a new shared definition introduced in the whole context and goal. In Ltac1, it would have been written as:

In Ltac2, we need to:

• **use lowercase for variables**
• use Control.hyp to recover the body of h
• Constr.type is now a proper function rather than an ad-hoc construction
• use the Fresh module to create fresh variables
• use $ to unquote variables back to Rocq's world
• use @ to create Rocq identifier

In the end, this gives us a script that is similar but with a few decorations and clearer semantics, which can be written with or without importing the modules.

The advantage of Ltac2 is that the FFI interface enables us to write scripts we could not have in Ltac1. For instance, we can now use the Constr.Unsafe API to write the simplify_let tactic by directly accessing the structure of the term, and performing the substitution by hand rather than relying on high-level tactics like lazy head beta. This can be seend by printing the resulting body.