Skip to content

Commit

Permalink
update README
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster committed Feb 29, 2024
1 parent c5b84fe commit 663c764
Showing 1 changed file with 9 additions and 0 deletions.
9 changes: 9 additions & 0 deletions time/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,15 @@ Tiny package which interacts with the `C++` implementation concerning time.

Require the package in your `lakefile.lean` and add `import Time` in your Lean file.

## Troubleshoot

If you get an error that `c++` is not found, you can double-check with `which c++ g++ gcc`
and then install `gcc` with:

```
sudo apt install build-essential
```

**Implemented Functions:**

- `Time.getLocalTime` returns the local date/time as a `String`.
Expand Down

0 comments on commit 663c764

Please sign in to comment.