Skip to content

Conversation

@DCupello1
Copy link

@DCupello1 DCupello1 commented Nov 13, 2025

This pull request is made to introduce the "improves-ids" pass.

This pass goes through all of the ids and makes sure that there is no ambiguity between names. It also gives names to anonymous constructors using the type name.

Some examples:

syntax bit = 
  | `%`{i : nat}(i : nat)
  
def $min(nat : nat, nat : nat) : nat
  def $min{i : nat, j : nat}(i, j) = i
    -- if (i <= j)
  def $min{i : nat, j : nat}(i, j) = j
    -- otherwise

to

syntax bit = 
  | mk_bit{i : nat}(i : nat)

def $min(nat : nat, nat_0 : nat) : nat
  def $min{i : nat, j : nat}(i, j) = i
    -- if (i <= j)
  def $min{i : nat, j : nat}(i, j) = j
    -- otherwise

Based off of #195 so will have to merge that one first.

@DCupello1
Copy link
Author

@nomeata
This pass now only focuses on disambiguation of ids, not adding explicit prefixes as before.

It now does not change ids based on a reserved list of names, since this was pretty Rocq-specific. You will probably have to do some sort of check in your lean translation.

@nomeata
Copy link

nomeata commented Nov 13, 2025

Thanks!

You will probably have to do some sort of check in your lean translation.

Right, I already have that

let render_id a = match a with
  | "mut" | "local" | "export" | "import" | "catch" | "syntax"
    -> "«" ^ a ^ "»"
  | _ -> a

@DCupello1 DCupello1 mentioned this pull request Dec 16, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants