HERMIT to HERMIT Shell - ku-fpg/hermit-shell GitHub Wiki

Symbols

	Meaning
:microphone:	implemented in server
:speaker:	implemented in client
:left_right_arrow:	tested by hand, front to back, implies :microphone: & :speaker:
:white_check_mark:	In a unit test. The test may or may not run

Types

HERMIT Type	HERMIT-shell Type	Notes
`RhsOfName`	`Name`
`TransformH :: * -> * -> *`	`Transform`
`LCoreTC`
`LocalPathH`	`LocalPath`
`RewriteH`	`Rewrite`

All shell functions

`HERMIT.Dictionary.AlphaConversion`

Name	Type	Done
`alpha`	`RewriteH LCore`	:microphone: :speaker:
`alpha-lam`	`String -> RewriteH LCore`	:white_check_mark:
`alpha-lam`	`RewriteH LCore`	:microphone: :speaker:
`alpha-case-binder`	`String -> RewriteH LCore`	:microphone: :speaker:
`alpha-case-binder`	`RewriteH LCore`	:microphone: :speaker:
`alpha-alt`	`RewriteH LCore`	:microphone: :speaker:
`alpha-alt`	`[String] -> RewriteH LCore`	:microphone: :speaker:
`alpha-case`	`RewriteH LCore`	:microphone: :speaker:
`alpha-let`	`[String] -> RewriteH LCore`	:microphone: :speaker:
`alpha-let`	`RewriteH LCore`	:microphone: :speaker:
`alpha-top`	`[String] -> RewriteH LCore`	:microphone: :speaker:
`alpha-top`	`RewriteH LCore`	:microphone: :speaker:
`alpha-prog`	`RewriteH LCore`	:microphone: :speaker:
`unshadow`	`RewriteH LCore`	:microphone: :speaker:

`HERMIT.Dictionary.Composite`

Name	Type	Done
`unfold-basic-combinator`	`RewriteH LCore`	:microphone: :speaker:
`simplify`	`RewriteH LCore`	:microphone: :speaker:
`bash`	`RewriteH LCore`	:white_check_mark:
`smash`	`RewriteH LCore`	:microphone: :speaker:
`bash-extended-with`	`[RewriteH LCore] -> RewriteH LCore`	:white_check_mark:
`smash-extended-with`	`[RewriteH LCore] -> RewriteH LCore`	:microphone: :speaker:
`bash-debug`	`RewriteH LCore`	:microphone: :speaker:

`HERMIT.Dictionary.Debug`

Name	Type	Done
`trace`	`String -> RewriteH LCoreTC`	:microphone: :speaker:
`observe`	`String -> RewriteH LCoreTC`	:microphone: :speaker:
`observe-failure`	`String -> RewriteH LCoreTC -> RewriteH LCoreTC`	:microphone: :speaker:
`bracket`	`String -> RewriteH LCoreTC -> RewriteH LCoreTC`	:microphone: :speaker:

`HERMIT.Dictionary.FixPoint`

Name	Type	Done
`fix-intro`	`RewriteH LCore`	:microphone: :speaker:
`fix-computation-rule`	`BiRewriteH LCore`	:microphone: :speaker:
`fix-rolling-rule`	`BiRewriteH LCore`	:microphone: :speaker:
`fix-fusion-rule`	`String -> String -> String -> RewriteH LCore -> RewriteH LCore -> RewriteH LCore -> BiRewriteH LCore`	:white_check_mark:
`fix-fusion-rule-unsafe`	`String -> String -> String -> RewriteH LCore -> BiRewriteH LCore`	:microphone: :speaker:
`fix-fusion-rule-unsafe`	`String -> String -> String -> BiRewriteH LCore`	:microphone: :speaker:

`HERMIT.Dictionary.Fold`

Name	Type	Done
`fold`	`HermitName -> RewriteH LCore`	:white_check_mark:

`HERMIT.Dictionary.Function`

Name	Type	Done
`static-arg`	`RewriteH LCore`	:microphone: :speaker:
`static-arg-types`	`RewriteH LCore`	:microphone: :speaker:
`static-arg-pos`	`[Int] -> RewriteH LCore`	:microphone: :speaker:

`HERMIT.Dictionary.GHC`

Name	Type	Done
`deshadow-prog`	`RewriteH LCore`	:microphone: :speaker:
`dezombify`	`RewriteH LCore`	:microphone: :speaker:
`occurrence-analysis`	`RewriteH LCore`	:microphone: :speaker:
`lint-expr`	`TransformH LCoreTC String`	:microphone: :speaker:
`lint-module`	`TransformH LCoreTC String`	:microphone: :speaker:
`lint`	`TransformH LCoreTC String`	:microphone: :speaker:
`load-lemma-library`	`HermitName -> TransformH LCore String`	:microphone: :speaker:
`load-lemma-library`	`HermitName -> LemmaName -> TransformH LCore String`	:microphone: :speaker:
`inject-dependency`	`String -> TransformH LCore ()`	:microphone: :speaker:

`HERMIT.Dictionary.Induction`

Name	Type	Done
`induction`	`HermitName -> RewriteH LCore`	:microphone: :speaker:
`prove-by-cases`	`HermitName -> RewriteH LCore`	:microphone: :speaker:

`HERMIT.Dictionary.Inline`

Name	Type	Done
`inline`	`RewriteH LCore`	:microphone: :speaker:
`inline`	`OccurrenceName -> RewriteH LCore`	:microphone: :speaker:
`inline`	`[String] -> RewriteH LCore`	:microphone: :speaker:
`inline-case-scrutinee`	`RewriteH LCore`	:microphone: :speaker:
`inline-case-alternative`	`RewriteH LCore`	:microphone: :speaker:

`HERMIT.Dictionary.Kure`

Name	Type	Done
`id`	`RewriteH LCore`	:microphone: :speaker:
`id`	`RewriteH LCoreTC`	:microphone: :speaker:
`success`	`TransformH LCore ()`	:microphone: :speaker:
`fail`	`String -> RewriteH LCore`	:microphone: :speaker:
`<+`	`RewriteH LCore -> RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`<+`	`TransformH LCore () -> TransformH LCore () -> TransformH LCore ()`	:microphone: :speaker:
`>>>`	`RewriteH LCore -> RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`>>>`	`BiRewriteH LCore -> BiRewriteH LCore -> BiRewriteH LCore`	:microphone: :speaker:
`>>>`	`RewriteH LCoreTC -> RewriteH LCoreTC -> RewriteH LCoreTC`	:microphone: :speaker:
`>+>`	`RewriteH LCore -> RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`try`	`RewriteH LCore -> RewriteH LCore`	:white_check_mark:
`repeat`	`RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`replicate`	`Int -> RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`all`	`RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`any`	`RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`one`	`RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`all-bu`	`RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`all-td`	`RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`all-du`	`RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`any-bu`	`RewriteH LCore -> RewriteH LCore`	:white_check_mark:
`any-td`	`RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`any-du`	`RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`one-td`	`RewriteH LCore -> RewriteH LCore`	:white_check_mark:
`one-bu`	`RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`prune-td`	`RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`innermost`	`RewriteH LCore -> RewriteH LCore`	:white_check_mark:
`focus`	`TransformH LCoreTC LocalPathH -> RewriteH LCoreTC -> RewriteH LCoreTC`	:microphone: :speaker:
`focus`	`TransformH LCoreTC LocalPathH -> TransformH LCoreTC String -> TransformH LCoreTC String`	:microphone: :speaker:
`focus`	`LocalPathH -> RewriteH LCoreTC -> RewriteH LCoreTC`	:microphone: :speaker:
`focus`	`LocalPathH -> TransformH LCoreTC String -> TransformH LCoreTC String`	:microphone: :speaker:
`focus`	`TransformH LCore LocalPathH -> RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`focus`	`TransformH LCore LocalPathH -> TransformH LCore String -> TransformH LCore String`	:microphone: :speaker:
`focus`	`LocalPathH -> RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`focus`	`LocalPathH -> TransformH LCore String -> TransformH LCore String`	:microphone: :speaker:
`when`	`TransformH LCore () -> RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`not`	`TransformH LCore () -> TransformH LCore ()`	:microphone: :speaker:
`invert`	`BiRewriteH LCore -> BiRewriteH LCore`	:microphone: :speaker:
`forward`	`BiRewriteH LCore -> RewriteH LCore`	:white_check_mark:
`backward`	`BiRewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`test`	`RewriteH LCore -> TransformH LCore String`	:microphone: :speaker:
`any-call`	`RewriteH LCore -> RewriteH LCore`	:white_check_mark:
`promote`	`RewriteH LCore -> RewriteH LCoreTC`	:microphone: :speaker:
`extract`	`RewriteH LCoreTC -> RewriteH LCore`	:microphone: :speaker:
`extract`	`TransformH LCoreTC String -> TransformH LCore String`	:microphone: :speaker:
`between`	`Int -> Int -> RewriteH LCoreTC -> RewriteH LCoreTC`	:microphone: :speaker:
`atPath`	`TransformH LCore LocalPathH -> TransformH LCore LCore`	:microphone: :speaker:
`atPath`	`TransformH LCoreTC LocalPathH -> TransformH LCoreTC LCoreTC`	:microphone: :speaker:
`atPath`	`TransformH LCoreTC LocalPathH -> TransformH LCore LCore`	:microphone: :speaker:

`HERMIT.Dictionary.Local.Bind`

Name	Type	Done
`nonrec-to-rec`	`RewriteH LCore`	:microphone: :speaker:
`rec-to-nonrec`	`RewriteH LCore`	:microphone: :speaker:

`HERMIT.Dictionary.Local.Case`

Name	Type	Done
`case-float-app`	`RewriteH LCore`	:microphone: :speaker:
`case-float-arg`	`RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`case-float-arg`	`CoreString -> RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`case-float-arg-unsafe`	`CoreString -> RewriteH LCore`	:microphone: :speaker:
`case-float-arg-unsafe`	`LemmaName -> RewriteH LCore`	:microphone: :speaker:
`case-float-arg-lemma`	`LemmaName -> RewriteH LCore`	:microphone: :speaker:
`case-float-case`	`RewriteH LCore`	:microphone: :speaker:
`case-float-cast`	`RewriteH LCore`	:microphone: :speaker:
`case-float-let`	`RewriteH LCore`	:microphone: :speaker:
`case-float`	`RewriteH LCore`	:microphone: :speaker:
`case-float-in`	`RewriteH LCore`	:microphone: :speaker:
`case-float-in-args`	`RewriteH LCore`	:microphone: :speaker:
`case-reduce`	`RewriteH LCore`	:microphone: :speaker:
`case-reduce-datacon`	`RewriteH LCore`	:microphone: :speaker:
`case-reduce-literal`	`RewriteH LCore`	:microphone: :speaker:
`case-reduce-unfold`	`RewriteH LCore`	:microphone: :speaker:
`case-split`	`OccurrenceName -> RewriteH LCore`	:microphone: :speaker:
`case-split`	`CoreString -> RewriteH LCore`	:microphone: :speaker:
`case-split-inline`	`OccurrenceName -> RewriteH LCore`	:white_check_mark:
`case-split-inline`	`CoreString -> RewriteH LCore`	:microphone: :speaker:
`case-intro-seq`	`String -> RewriteH LCore`	:microphone: :speaker:
`case-elim-seq`	`RewriteH LCore`	:microphone: :speaker:
`case-inline-alternative`	`RewriteH LCore`	:microphone: :speaker:
`case-inline-scrutinee`	`RewriteH LCore`	:microphone: :speaker:
`case-merge-alts`	`RewriteH LCore`	:microphone: :speaker:
`case-merge-alts-with-binder`	`RewriteH LCore`	:microphone: :speaker:
`case-elim`	`RewriteH LCore`	:white_check_mark:
`case-elim-inline-scrutinee`	`RewriteH LCore`	:microphone: :speaker:
`case-elim-merge-alts`	`RewriteH LCore`	:white_check_mark:
`case-fold-binder`	`RewriteH LCore`	:microphone: :speaker:

`HERMIT.Dictionary.Local.Cast`

Name	Type	Done
`cast-elim`	`RewriteH LCore`	:microphone: :speaker:
`cast-elim-refl`	`RewriteH LCore`	:microphone: :speaker:
`cast-elim-sym`	`RewriteH LCore`	:microphone: :speaker:
`cast-elim-sym-plus`	`RewriteH LCore`	:microphone: :speaker:
`cast-float-app`	`RewriteH LCore`	:microphone: :speaker:
`cast-float-lam`	`RewriteH LCore`	:microphone: :speaker:
`cast-elim-unsafe`	`RewriteH LCore`	:microphone: :speaker:

`HERMIT.Dictionary.Local.Let`

Name	Type	Done
`let-subst`	`RewriteH LCore`	:white_check_mark:
`let-subst-safe`	`RewriteH LCore`	:microphone: :speaker:
`let-nonrec-subst-safe`	`RewriteH LCore`	:microphone: :speaker:
`let-intro`	`String -> RewriteH LCore`	:white_check_mark:
`let-intro-unfolding`	`HermitName -> RewriteH LCore`	:microphone: :speaker:
`let-elim`	`RewriteH LCore`	:white_check_mark:
`let-float-app`	`RewriteH LCore`	:microphone: :speaker:
`let-float-arg`	`RewriteH LCore`	:microphone: :speaker:
`let-float-lam`	`RewriteH LCore`	:microphone: :speaker:
`let-float-let`	`RewriteH LCore`	:microphone: :speaker:
`let-float-case`	`RewriteH LCore`	:microphone: :speaker:
`let-float-case-alt`	`RewriteH LCore`	:microphone: :speaker:
`let-float-case-alt`	`Int -> RewriteH LCore`	:microphone: :speaker:
`let-float-cast`	`RewriteH LCore`	:microphone: :speaker:
`let-float-top`	`RewriteH LCore`	:microphone: :speaker:
`let-float`	`RewriteH LCore`	:microphone: :speaker:
`let-to-case`	`RewriteH LCore`	:microphone: :speaker:
`let-float-in`	`RewriteH LCore`	:microphone: :speaker:
`let-float-in-app`	`RewriteH LCore`	:microphone: :speaker:
`let-float-in-case`	`RewriteH LCore`	:microphone: :speaker:
`let-float-in-lam`	`RewriteH LCore`	:microphone: :speaker:
`reorder-lets`	`[String] -> RewriteH LCore`	:white_check_mark:
`let-tuple`	`String -> RewriteH LCore`	:white_check_mark:
`prog-bind-elim`	`RewriteH LCore`	:microphone: :speaker:
`prog-bind-nonrec-elim`	`RewriteH LCore`	:microphone: :speaker:
`prog-bind-rec-elim`	`RewriteH LCore`	:microphone: :speaker:

`HERMIT.Dictionary.Local`

Name	Type	Done
`beta-reduce`	`RewriteH LCore`	:microphone: :speaker:
`beta-expand`	`RewriteH LCore`	:white_check_mark:
`eta-reduce`	`RewriteH LCore`	:microphone: :speaker:
`eta-expand`	`String -> RewriteH LCore`	:white_check_mark:
`flatten-module`	`RewriteH LCore`	:white_check_mark:
`flatten-program`	`RewriteH LCore`	:microphone: :speaker:
`abstract`	`OccurrenceName -> RewriteH LCore`	:white_check_mark:
`push`	`String -> RewriteH LCore -> RewriteH LCore`	:white_check_mark:
`push-unsafe`	`String -> RewriteH LCore`	:microphone: :speaker:

`HERMIT.Dictionary.Navigation.Crumbs`

Name	Type	Done
`prog`	`Crumb`	:microphone: :speaker:
`prog-head`	`Crumb`	:microphone: :speaker:
`prog-tail`	`Crumb`	:microphone: :speaker:
`nonrec-rhs`	`Crumb`	:microphone: :speaker:
`rec-def`	`Crumb`	:microphone: :speaker:
`def-rhs`	`Crumb`	:white_check_mark:
`app-fun`	`Crumb`	:microphone: :speaker:
`app-arg`	`Crumb`	:white_check_mark:
`lam-body`	`Crumb`	:white_check_mark:
`let-bind`	`Crumb`	:microphone: :speaker:
`let-body`	`Crumb`	:white_check_mark:
`case-expr`	`Crumb`	:microphone: :speaker:
`case-type`	`Crumb`	:microphone: :speaker:
`case-alt`	`Int -> Crumb`	:white_check_mark:
`cast-expr`	`Crumb`	:microphone: :speaker:
`cast-co`	`Crumb`	:microphone: :speaker:
`tick-expr`	`Crumb`	:microphone: :speaker:
`alt-rhs`	`Crumb`	:white_check_mark:
`type`	`Crumb`	:microphone: :speaker:
`coercion`	`Crumb`	:microphone: :speaker:
`appTy-fun`	`Crumb`	:microphone: :speaker:
`appTy-arg`	`Crumb`	:microphone: :speaker:
`tyCon-arg`	`Crumb`	:microphone: :speaker:
`fun-dom`	`Crumb`	:microphone: :speaker:
`fun-cod`	`Crumb`	:microphone: :speaker:
`forall-body`	`Crumb`	:microphone: :speaker:
`refl-type`	`Crumb`	:microphone: :speaker:
`coCon-arg`	`Crumb`	:microphone: :speaker:
`appCo-fun`	`Crumb`	:microphone: :speaker:
`appCo-arg`	`Crumb`	:microphone: :speaker:
`coForall-body`	`Crumb`	:microphone: :speaker:
`axiom-inst`	`Crumb`	:microphone: :speaker:
`unsafe-left`	`Crumb`	:microphone: :speaker:
`unsafe-right`	`Crumb`	:microphone: :speaker:
`sym-co`	`Crumb`	:microphone: :speaker:
`trans-left`	`Crumb`	:microphone: :speaker:
`trans-right`	`Crumb`	:microphone: :speaker:
`nth-co`	`Crumb`	:microphone: :speaker:
`inst-co`	`Crumb`	:microphone: :speaker:
`inst-type`	`Crumb`	:microphone: :speaker:
`lr-co`	`Crumb`	:microphone: :speaker:
`forall-body`	`Crumb`	:microphone: :speaker:
`conj-lhs`	`Crumb`	:microphone: :speaker:
`conj-rhs`	`Crumb`	:microphone: :speaker:
`disj-lhs`	`Crumb`	:microphone: :speaker:
`disj-rhs`	`Crumb`	:microphone: :speaker:
`antecedent`	`Crumb`	:microphone: :speaker:
`consequent`	`Crumb`	:microphone: :speaker:
`eq-lhs`	`Crumb`	:microphone: :speaker:
`eq-rhs`	`Crumb`	:microphone: :speaker:

`HERMIT.Dictionary.Navigation`

Name	Type	Done
`rhs-of`	`RhsOfName -> TransformH LCoreTC LocalPathH`	:white_check_mark:
`binding-group-of`	`String -> TransformH LCoreTC LocalPathH`	:microphone: :speaker:
`binding-of`	`BindingName -> TransformH LCoreTC LocalPathH`	:white_check_mark:
`occurrence-of`	`OccurrenceName -> TransformH LCoreTC LocalPathH`	:microphone: :speaker:
`application-of`	`OccurrenceName -> TransformH LCoreTC LocalPathH`	:microphone: :speaker:
`consider`	`Considerable -> TransformH LCore LocalPathH`	:white_check_mark:
`arg`	`Int -> TransformH LCore LocalPathH`	:microphone: :speaker:
`lams-body`	`TransformH LCore LocalPathH`	:microphone: :speaker:
`lets-body`	`TransformH LCore LocalPathH`	:microphone: :speaker:
`prog-end`	`TransformH LCore LocalPathH`	:microphone: :speaker:
`parent-of`	`TransformH LCore LocalPathH -> TransformH LCore LocalPathH`	:microphone: :speaker:
`parent-of`	`TransformH LCoreTC LocalPathH -> TransformH LCoreTC LocalPathH`	:microphone: :speaker:

`HERMIT.Dictionary.New`

Name	Type	Done
`var`	`String -> TransformH LCore ()`	:microphone: :speaker:
`nonrec-intro`	`String -> CoreString -> RewriteH LCore`	:microphone: :speaker:

`HERMIT.Dictionary.Query`

Name	Type	Done
`info`	`TransformH LCoreTC String`	:microphone: :speaker:
`compare-bound-ids`	`HermitName -> HermitName -> TransformH LCoreTC ()`	:microphone: :speaker:
`compare-core-at`	`TransformH LCoreTC LocalPathH -> TransformH LCoreTC LocalPathH -> TransformH LCoreTC ()`	:microphone: :speaker:

`HERMIT.Dictionary.Reasoning`

Name	Type	Done
`retraction`	`CoreString -> CoreString -> RewriteH LCore -> BiRewriteH LCore`	:microphone: :speaker:
`retraction-unsafe`	`CoreString -> CoreString -> BiRewriteH LCore`	:microphone: :speaker:
`unshadow-quantified`	`RewriteH LCoreTC`	:microphone: :speaker:
`merge-quantifiers`	`RewriteH LCore`	:microphone: :speaker:
`float-left`	`RewriteH LCore`	:microphone: :speaker:
`float-right`	`RewriteH LCore`	:microphone: :speaker:
`conjunct`	`LemmaName -> LemmaName -> LemmaName -> Transform LCore ()`	:microphone: :speaker:
`disjunct`	`LemmaName -> LemmaName -> LemmaName -> Transform LCore ()`	:microphone: :speaker:
`imply`	`LemmaName -> LemmaName -> LemmaName -> Transform LCore ()`	:microphone: :speaker:
`lemma-birewrite`	`LemmaName -> BiRewriteH LCore`	:microphone: :speaker:
`lemma-forward`	`LemmaName -> RewriteH LCore`	:microphone: :speaker:
`lemma-backward`	`LemmaName -> RewriteH LCore`	:microphone: :speaker:
`lemma-consequent`	`LemmaName -> RewriteH LCore`	:microphone: :speaker:
`lemma-consequent-birewrite`	`LemmaName -> BiRewriteH LCore`	:microphone: :speaker:
`lemma-lhs-intro`	`LemmaName -> RewriteH LCore`	:microphone: :speaker:
`lemma-rhs-intro`	`LemmaName -> RewriteH LCore`	:microphone: :speaker:
`inst-lemma`	`LemmaName -> HermitName -> CoreString -> TransformH LCore ()`	:microphone: :speaker:
`inst-dictionaries`	`RewriteH LCore`	:microphone: :speaker:
`abstract-forall`	`String -> CoreString -> RewriteH LCore`
`abstract-forall`	`String -> RewriteH LCore -> RewriteH LCore`
`copy-lemma`	`TransformH LCore ()`	:microphone: :speaker:
`modify-lemma`	`LemmaName -> RewriteH LCore -> TransformH LCore ()`	:microphone: :speaker:
`query-lemma`	`LemmaName -> TransformH LCore String -> TransformH LCore String`	:microphone: :speaker:
`show-lemma`	`PrettyPrinter -> LemmaName -> PrettyH LCore`
`show-lemmas`	`PrettyPrinter -> LemmaName -> PrettyH LCore`
`show-lemmas`	`PrettyPrinter -> PrettyH LCore`
`extensionality`	`String -> RewriteH LCore`	:microphone: :speaker:
`extensionality`	`RewriteH LCore`	:microphone: :speaker:
`lhs`	`TransformH LCore String -> TransformH LCore String`	:microphone: :speaker:
`lhs`	`RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`rhs`	`TransformH LCore String -> TransformH LCore String`	:microphone: :speaker:
`rhs`	`RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`both`	`RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`both`	`TransformH LCore String -> TransformH LCore String`	:microphone: :speaker:
`reflexivity`	`RewriteH LCore`	:microphone: :speaker:
`simplify-lemma`	`RewriteH LCore`	:microphone: :speaker:
`split-antecedent`	`RewriteH LCore`	:microphone: :speaker:
`lemma`	`LemmaName -> RewriteH LCore`	:microphone: :speaker:
`lemma-unsafe`	`LemmaName -> RewriteH LCore`	:microphone: :speaker:

`HERMIT.Dictionary.Remembered`

Name	Type	Done
`remember`	`LemmaName -> TransformH LCore ()`	:white_check_mark:
`unfold-remembered`	`LemmaName -> RewriteH LCore`	:white_check_mark:
`fold-remembered`	`LemmaName -> RewriteH LCore`	:white_check_mark:
`fold-any-remembered`	`RewriteH LCore`	:microphone: :speaker:
`show-remembered`	`PrettyPrinter -> PrettyH LCore`

`HERMIT.Dictionary.Rules`

Name	Type	Done
`show-rules`	`TransformH LCoreTC String`	:microphone: :speaker:
`show-rule`	`PrettyPrinter -> RuleName -> TransformH LCoreTC DocH`
`fold-rule`	`RuleName -> RewriteH LCore`	:microphone: :speaker:
`fold-rules`	`[RuleName] -> RewriteH LCore`	:microphone: :speaker:
`unfold-rule`	`RuleName -> RewriteH LCore`	:microphone: :speaker:
`unfold-rule-unsafe`	`RuleName -> RewriteH LCore`	:microphone: :speaker:
`unfold-rules`	`[RuleName] -> RewriteH LCore`	:microphone: :speaker:
`unfold-rules-unsafe`	`[RuleName] -> RewriteH LCore`	:white_check_mark:
`rule-to-lemma`	`PrettyPrinter -> RuleName -> TransformH LCore DocH`
`spec-constr`	`RewriteH LCore`	:microphone: :speaker:
`specialise`	`RewriteH LCore`	:microphone: :speaker:

`HERMIT.Dictionary.Undefined`

Name	Type	Done
`replace-current-expr-with-undefined`	`RewriteH LCore`	:microphone: :speaker:
`replace-id-with-undefined`	`HermitName -> RewriteH LCore`	:microphone: :speaker:
`error-to-undefined`	`RewriteH LCore`	:microphone: :speaker:
`is-undefined-val`	`TransformH LCore ()`	:microphone: :speaker:
`undefined-expr`	`RewriteH LCore`	:microphone: :speaker:
`undefined-app`	`RewriteH LCore`	:microphone: :speaker:
`undefined-lam`	`RewriteH LCore`	:microphone: :speaker:
`undefined-let`	`RewriteH LCore`	:microphone: :speaker:
`undefined-case`	`RewriteH LCore`	:white_check_mark:
`undefined-cast`	`RewriteH LCore`	:microphone: :speaker:
`undefined-tick`	`RewriteH LCore`	:microphone: :speaker:

`HERMIT.Dictionary.Unfold`

Name	Type	Done
`beta-reduce-plus`	`RewriteH LCore`	:microphone: :speaker:
`unfold`	`RewriteH LCore`	:microphone: :speaker:
`unfold`	`OccurrenceName -> RewriteH LCore`	:white_check_mark:
`unfold`	`[OccurrenceName] -> RewriteH LCore`	:microphone: :speaker:
`unfold-saturated`	`RewriteH LCore`	:microphone: :speaker:
`specialize`	`RewriteH LCore`	:microphone: :speaker:

`HERMIT.Dictionary.Unsafe`

Name	Type	Done
`unsafe-replace`	`CoreString -> RewriteH LCore`	:microphone: :speaker:

`HERMIT.Dictionary.WorkerWrapper.Common`

Name	Type	Done
`intro-ww-assumption-A`		:microphone: :speaker:
`intro-ww-assumption-B`		:microphone: :speaker:
`intro-ww-assumption-C`		:microphone: :speaker:
`split-1-beta`	`CoreString -> RewriteH LCore`	:microphone: :speaker:
`split-2-beta`	`CoreString -> RewriteH LCore`	:microphone: :speaker:

`HERMIT.Dictionary.WorkerWrapper.Fix`

Name	Type	Done
`ww-factorisation-unsafe`	`String -> String -> BiRewriteH LCore`	:microphone: :speaker:
`ww-split-unsafe`		:microphone: :speaker:
`ww-assumption-B`		:microphone: :speaker:
`ww-assumption-A-unsafe`		:microphone: :speaker:
`ww-assumption-C-unsafe`		:microphone: :speaker:
`ww-AssA-to-AssB`	`RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`ww-AssB-to-AssC`	`RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`ww-AssA-to-AssC`	`RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`ww-generate-fusion`	`RewriteH LCore -> TransformH LCore ()`	:microphone: :speaker:
`ww-generate-fusion-unsafe`	`TransformH LCore ()`	:microphone: :speaker:
`ww-fusion`	`BiRewriteH LCore`	:microphone: :speaker:

`HERMIT.Dictionary.WorkerWrapper.FixResult`

Name	Type	Done
`ww-result-factorisation`	`String -> String -> RewriteH LCore -> BiRewriteH LCore`	:microphone: :speaker:
`ww-result-factorisation-unsafe`	`String -> String -> BiRewriteH LCore`	:microphone: :speaker:
`ww-split-static-arg-unsafe`	`Int -> [Int] -> String -> String -> RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`ww-result-split`	`String -> String -> RewriteH LCore -> RewriteH LCore`	:white_check_mark:
`ww-result-split-unsafe`	`String -> String -> RewriteH LCore`	:microphone: :speaker:
`ww-result-split-static-arg`	`Int -> [Int] -> String -> String -> RewriteH LCore -> RewriteH LCore`	:white_check_mark:
`ww-result-split-static-arg-unsafe`	`Int -> [Int] -> String -> String -> RewriteH LCore`	:microphone: :speaker:
`ww-result-assumption-A`	`String -> String -> RewriteH LCore -> BiRewriteH LCore`	:microphone: :speaker:
`ww-result-assumption-B`	`String -> String -> String -> RewriteH LCore -> BiRewriteH LCore`	:microphone: :speaker:
`ww-result-assumption-C`	`String -> String -> String -> RewriteH LCore -> BiRewriteH LCore`	:microphone: :speaker:
`ww-result-assumption-A-unsafe`	`String -> String -> BiRewriteH LCore`	:microphone: :speaker:
`ww-result-assumption-B-unsafe`	`String -> String -> String -> BiRewriteH LCore`	:microphone: :speaker:
`ww-result-assumption-C-unsafe`	`String -> String -> String -> BiRewriteH LCore`	:microphone: :speaker:
`ww-result-AssA-to-AssB`	`RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`ww-result-AssB-to-AssC`	`RewriteH LCore -> RewriteH LCore`	:microphone: :speaker:
`ww-result-AssA-to-AssC`	`RewriteH LCore -> RewriteH LCore`	:white_check_mark:
`ww-result-generate-fusion`	`RewriteH LCore -> TransformH LCore ()`	:microphone: :speaker:
`ww-result-generate-fusion-unsafe`	`TransformH LCore ()`	:microphone: :speaker:
`ww-result-fusion`	`BiRewriteH LCore`	:white_check_mark:

`HERMIT.PrettyPrinter.AST`

Name	Type	Done
`ast`

`HERMIT.PrettyPrinter.Clean`

Name	Type	Done
`clean`

`HERMIT.PrettyPrinter.GHC`

Name	Type	Done
`ghc`

`HERMIT.Shell.Dictionary`

Name	Type	Done
`help`
`help`

`HERMIT.Shell.Externals`

Name	Type	Done
`resume`	`ShellEffect`	:microphone: :speaker:
`abort`	`ShellEffect`	:microphone: :speaker:
`continue`	`ShellEffect`	:microphone: :speaker:
`gc`
`gc`
`display`		:microphone: :speaker:
`up`	`KernelEffect`	:microphone: :speaker:
`navigate`
`command-line`
`set-window`	`ShellEffect`	:microphone: :speaker:
`top`	`KernelEffect`	:microphone: :speaker:
`log`	`QueryFun`	:microphone: :speaker:
`back`	`ShellEffect`	:microphone: :speaker:
`step`	`ShellEffect`	:microphone: :speaker:
`goto`
`goto`
`tag`	`String -> ShellEffect`	:microphone: :speaker:
`diff`	`AST -> AST -> QueryFun`	:microphone: :speaker:
`set-pp-diffonly`	`Bool -> ShellEffect`	:microphone: :speaker:
`set-fail-hard`	`Bool -> ShellEffect`	:microphone: :speaker:
`set-auto-corelint`	`Bool -> ShellEffect`	:microphone: :speaker:
`set-pp`	`String -> ShellEffect`	:microphone: :speaker:
`set-pp-renderer`
`set-pp-renderer`
`dump`	`String -> PrettyPrinter -> String -> Int -> ShellEffect`
~~`dump`~~	~~`String -> String -> Int -> ShellEffect`~~	(was deprecated)
~~`dump-lemma`~~	~~`LemmaName -> FilePath -> PrettyPrinter -> String -> Int -> TransformH LCoreTC ()`~~	(subsumed by the `dump-lemma` below)
`dump-lemma`	`PrettyPrinter -> LemmaName -> FilePath -> String -> Int -> TransformH LCoreTC ()`
`set-pp-width`	`Int -> ShellEffect`	:microphone: :speaker:
`set-pp-type`	`PpType -> ShellEffect`	:microphone: :speaker:
`set-pp-coercion`	`PpType -> ShellEffect`	:microphone: :speaker:
`set-pp-uniques`	`Bool -> ShellEffect`	:microphone: :speaker:
`{`	`KernelEffect`	:white_check_mark:
`}`	`KernelEffect`	:white_check_mark:
`load`	`String -> String -> ScriptEffect`	:microphone: :speaker:
`load-and-run`	`String -> ScriptEffect`	:microphone: :speaker:
`save`	`String -> ScriptEffect`	:microphone: :speaker:
`save-verbose`	`String -> ScriptEffect`	:microphone: :speaker:
`save-script`	`String -> String -> ScriptEffect`	:microphone: :speaker:
`load-as-rewrite`	`String -> String -> ScriptEffect`	:microphone: :speaker:
`script-to-rewrite`		:microphone: :speaker:
`define-script`		:microphone: :speaker:
`define-rewrite`		:microphone: :speaker:
`run-script`		:microphone: :speaker:
`display-scripts`		:microphone: :speaker:
`stop-script`		:microphone: :speaker:
`possible-rewrites`	`CommandLineState -> TransformH LCore String`

`HERMIT.Shell.Proof`

Name	Type	Done
`prove-lemma`	`LemmaName -> ShellEffect`	:white_check_mark:
`end-proof`	`ProofShellCommand`	:microphone: :speaker:
`end-case`	`ProofShellCommand`	:microphone: :speaker:
`assume`	`ProofShellCommand`	:white_check_mark: