Pas sûr si c'est mieux, mais tu devrais pouvoir faire ce qu'on fait pour les booléens (via `predef_names` in `src/builtin.ml`).
Comme discuté, je pense que ce serait pas trivial d'implémenter ça car le type `Interval` et les fonctions `eq_eq` et `eq_uneq` sont référencés dans des endroits où on a pas accès au contexte d’élaboration (ce qui est nécessaire pour utiliser la fonction `get_predef`).
OK, je suis allé voir pourquoi on a besoin du elab_context:
let get_predef (name: string) (ctx: DB.elab_context) : lexp = try let r = (DB.get_size ctx) - !builtin_size - 0 in let p = SMap.find name (!predef_map) in mkSusp p (S.shift r) with Not_found -> log_raise_error {|"%s" was not predefined|} name
[...ailleurs...]
let get_size (ctx : elab_context) = let (_, (n, _), lctx, _, _) = ctx in assert (n = M.length lctx); n
donc on a besoin du elab_context parce que `DB.get_size` prend un `elab_context` pour en extraire le `n` qui contient la taille du `lexp_context`, mais on pourrait aussi le calculer sur la base du `lexp_context`, sauf que c'est O(log N) au lieu de O(1).
:-(
Et tout ça pour faire un `S.shift` que l'on pourrait complètement éviter en évitant les indices de DeBruijn dans les predefs :-)
Je remarque cependant que t'as seulement besoin de `DB.eq_eq` (qui remplace `DB.eq_refl`) mais pas de `DB.eq_uneq`, donc on peut éliminer la définition en OCaml du type de `eq_uneq`.
Stefan