Pantograph

fix: Delayed MVars in MetaTranslate

1

#110 by aniva was merged 2024-10-09 18:08:10 -07:00

dev

bug/frontend-translate-delayed-mvar

TACAS '25

fix: Tactics should produce .syntheticOpaque goals

1

#100 by aniva was merged 2024-10-03 08:47:31 -07:00

dev

goal/tactic

0.2.19

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

fix: aux lemmas in env inspect

#82 by aniva was merged 2024-06-23 13:33:35 -07:00

dev

env/inspect

fix: Option setting in REPL

category

bug

#71 by aniva was merged 2024-04-15 12:58:08 -07:00

dev

lib/mkOptions

0.3

fix: Prevent incorrect inheritance of calc rhs

#66 by aniva was merged 2024-04-12 20:52:18 -07:00

dev

goal/calc

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

fix: Instantiation causes infinite loop

#54 by aniva was merged 2024-03-31 16:43:53 -07:00

dev

output/expr

fix: Build failure on macOS due to LLVM version

#53 by aniva was merged 2024-03-30 00:07:27 -07:00

dev

misc/toolchain

0.3

fix: Printing projection leads to crash

category

bug

part/Serial

#37 by aniva was merged 2023-12-07 12:33:02 -08:00

dev

io/sexp

0.2.10

fix: Rectify error format

category

bug

part/Goal

#31 by aniva was merged 2023-11-25 14:26:48 -08:00

dev

misc/error

Fix inconsistent sort level printing

category

bug

part/Serial

#12 by aniva was merged 2023-08-28 17:29:28 -07:00

dev

io/serial

0.2.4

Labels Milestones