diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/ExtractBase.ml | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 0a5d7df2..14ce4119 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -539,6 +539,16 @@ type extraction_ctx = { use it. Also see {!names_map.opaque_ids}. *) + use_dep_ite : bool; + (** For Lean: do we use dependent-if then else expressions? + + Example: + {[ + if h: b then ... else ... + -- ^^ + -- makes the if then else dependent + ]} + *) } (** Debugging function, used when communicating name collisions to the user, |