Pantograph

Add unsafe detection in goal.print

#151 opened 2024-12-19 05:02:52 -08:00 by aniva

Allow LSP-like behaviour of finding definition location via symbol

category

feature

part/Frontend

#150 opened 2024-12-19 05:02:20 -08:00 by aniva 0.2.24

Move Tactics to a Standalone Library

category

feature

part/Goal

#147 opened 2024-12-14 18:43:51 -08:00 by aniva 0.3

Pickle new constants generated in proof state

#142 opened 2024-12-10 21:48:42 -08:00 by aniva 0.3

Pickle environment extensions

#137 opened 2024-12-08 16:11:48 -08:00 by aniva

Proof state merger

1

#132 opened 2024-12-05 15:34:19 -08:00 by aniva

Drafting tactic in goals

#127 opened 2024-11-26 11:31:35 -08:00 by aniva 0.3

One stop env add

#117 opened 2024-10-22 11:02:32 -07:00 by aniva

goal.delete exceeds max recursion depth

1

#104 opened 2024-10-03 15:49:01 -07:00 by aniva

Timeout for tactics

category

feature

part/Goal

1

#102 opened 2024-09-09 23:49:44 -07:00 by aniva

Use MLList from Batteries

1

#98 opened 2024-09-08 13:39:37 -07:00 by aniva

Add option for Meta.ppGoal

#78 opened 2024-06-10 13:03:06 -07:00 by aniva

Printing fine-grained delaboration structure

1

#23 opened 2023-10-26 22:52:48 -07:00 by aniva io/serial

Labels Milestones