lean4-htt/src/Lean/Widget
2022-05-31 00:07:56 +02:00
..
Basic.lean feat: add Widget.Basic 2022-05-12 08:38:09 -07:00
InteractiveCode.lean feat: set tagAppFns in explicit exprToInteractive 2022-05-31 00:07:56 +02:00
InteractiveDiagnostic.lean refactor: auto-derive RpcEncoding 2022-05-12 13:22:37 -07:00
InteractiveGoal.lean fix: use consistent goal prefix everywhere 2022-05-09 17:49:00 +02:00
TaggedText.lean feat: add Widget.Basic 2022-05-12 08:38:09 -07:00