First, make sure to have Lean 4 properly set up. Then, to compile everything, navigate to this project's root directory in a terminal and run
> lake buildvoilà!
bracevac/path-dependent
Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|
| Name | Name | Last commit date | ||
|---|---|---|---|---|
First, make sure to have Lean 4 properly set up. Then, to compile everything, navigate to this project's root directory in a terminal and run
> lake buildvoilà!