Pantograph

test(repl): MVar name mismatch fix

#227 by aniva was merged 2025-07-02 15:03:10 -07:00

dev

chore/toolchain

0.3.4

feat(goal): Branch unification

2

#217 by aniva was merged 2025-06-24 13:56:15 -07:00

dev

goal/branch-unification

0.3.3

fix(goal): Name generation not available due to context

#174 by aniva was merged 2025-03-14 16:48:17 -07:00

dev

goal/tactic

0.3

chore: Version bump

#168 by aniva was merged 2025-02-25 15:16:44 -08:00

dev

chore/version

0.3

chore: Update Lean to v4.15.0

3

#134 by aniva was merged 2025-01-13 12:28:50 -08:00

dev

misc/version

0.2.25

chore: Update lean4-nix to mainline

#121 by aniva was merged 2024-11-15 17:44:02 -08:00

dev

misc/build

0.2.20

doc: Change license to Apache2

#116 by aniva was merged 2024-10-21 10:14:40 -07:00

dev

misc/license

0.2.20

feat: Error reporting in frontend

#107 by aniva was merged 2024-10-05 22:39:24 -07:00

dev

frontend/error

TACAS '25

doc: Add GPL License

#96 by aniva was merged 2024-09-07 14:12:34 -07:00

dev

misc/license

0.3

fix: Instantiate type when detecting eq

#91 by aniva was merged 2024-09-03 19:19:10 -07:00

dev

bug/eq-detection-in-congruence

fix: Bindings in prograde tactics

#90 by aniva was merged 2024-09-03 18:15:58 -07:00

dev

bug/hidden-fvar-in-define

fix: Resume not taking type unification into account

1

#89 by aniva was closed 2024-09-02 19:43:36 -07:00

dev

bug/resume-type-unification

0.3

chore: Update Lean to v4.10.0-rc1

#86 by aniva was merged 2024-07-06 21:37:30 -07:00

dev

misc/version

refactor: Cleanup the congruence tactics

#81 by aniva was merged 2024-06-23 13:35:36 -07:00

dev

tactic/congruence

0.3

chore: Version bump to v4.8.0-rc1

#75 by aniva was merged 2024-05-17 20:32:30 -07:00

dev

misc/version

0.3

feat: Elementarized tactics with motives, congruence, and absurdity

6

#72 by aniva was merged 2024-06-12 13:52:46 -07:00

dev

goal/mapply

feat: Print precursor rules in env/inspect

#65 by aniva was merged 2024-04-11 15:35:15 -07:00

dev

env/inspect

0.3

fix: Serialization of projection operators

#64 by aniva was merged 2024-04-09 21:28:53 -07:00

dev

serial/projection

0.3

fix: Auto bound implicit in elab

#60 by aniva was merged 2024-04-06 22:04:32 -07:00

dev

elab/level

0.3

test: Parallel testing infrastructure

#58 by aniva was merged 2024-04-06 14:16:46 -07:00

dev

misc/testing

Labels Milestones