WIP: log #39

Closed

rhi wants to merge 0 commits from log into 🐉

rhi commented

2024-01-13 09:33:11 -05:00

Owner

👉 #40

git machine broke

👉 #40 git machine broke

rhi added 10 commits 2024-01-13 09:33:12 -05:00

85fbb72e89 add algebraic ornaments to bib

430cfd05a6 fill a stray hole

368e63f614 fix some comments

547876205f move NDefinition to Quox.Definition and add an untyped one

09b34c81e2 refactor Main a whole lot

ff04348683 remove most noLocs

00716e9aba remove some unneeded Ord impls

88355bf469 reject "" in NatExtra.fromHex

b804ceb8fe happy new year [pack update. also idris 0.7.0]

2de2bd1f04 wip

rhi force-pushed log from 2de2bd1f04 to 8b8bec250a

2024-02-10 04:16:35 -05:00

Compare

rhi commented

2024-02-10 05:22:28 -05:00

Author

Owner

quox -P check fin.quox

on 🐉 branch: 0.253 s
on this branch: 4.154 s

ughhhhh

`quox -P check fin.quox` - on 🐉 branch: 0.253 s - on this branch: 4.154 s ughhhhh

rhi force-pushed log from 8b8bec250a to 979f972759

2024-03-27 13:01:27 -04:00

Compare

rhi force-pushed log from 979f972759 to 271e7f4519

2024-04-04 13:24:11 -04:00

Compare

rhi force-pushed log from 271e7f4519 to 3b6ae36e4e

2024-04-04 13:26:47 -04:00

Compare

rhi closed this pull request

2024-04-04 13:27:13 -04:00

rhi referenced this pull request

2024-04-04 13:29:45 -04:00

debug logging #40

Pull request closed

This pull request cannot be reopened because the branch was deleted.

No reviewers

No Label

No Milestone

No Assignees

1 Participants

Notifications

Due Date

The due date is invalid or out of range. Please use the format 'yyyy-mm-dd'.

No due date set.

Dependencies

No dependencies set.

Reference: rhi/quox#39

No description provided.