search

argumentcomputer / yatima

A zero-knowledge Lean4 compiler and kernel
MIT License
121 stars 9 forks source link

Use strings for Lurk names #189

Closed arthurpaulino closed 2 years ago

arthurpaulino commented 2 years ago

We currently use Lean.Name to represent symbol names in Lurk. While this makes it easier to transpile code compiled from Lean 4 sources, it's also messy because Lurk names don't follow the same rules as the (hierarchical) names in Lean.

Let's replace the usage of Lean names by regular strings in the entire Lurk AST.

This issue goes hand in hand with the following task: replace the try-hard fixes to achieve valid Lurk names by escaping pipes during transpilation.

winston-h-zhang commented 2 years ago

@arthurpaulino Is this still going to be a goal since I think John mentioned that Lurk intends to have hierarchal names in the future?

arthurpaulino commented 2 years ago

Right, I think we can close it. At least for now