0.2.10

New Issue

Minor serialization update:

Print Expr.proj as function applications w.r.t. the projector of a structure
Print "private" symbols, which proofs somehow depend on, in the catalog. However unsafe and symbols in the Lean. namespace should not be printed.

2023-12-05

100% Completed

test: Deserialization

#42 by aniva was merged 2024-01-08 12:21:45 -08:00

feat: Change the main interaction monad

#40 by aniva was merged 2023-12-14 05:46:40 -08:00

The main interaction monad should be MetaM and not TermElabM

#39 by aniva was closed 2023-12-26 12:46:14 -08:00 core/loop

fix: Printing projection leads to crash

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

feat: Print structural projection as application

#35 by aniva was merged 2023-12-05 20:20:52 -08:00

Print structures

#34 by aniva was closed 2024-01-08 12:24:00 -08:00 io/serial

The option on GoalTacticResult.goals? is redundant

#24 by aniva was closed 2024-01-16 14:20:31 -08:00