HERMIT to HERMIT Shell

Symbols

	Meaning
🎤	implemented in server
🔈	implemented in client
↔️	tested by hand, front to back, implies 🎤 & 🔈
✅	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`	🎤 🔈
`alpha-lam`	`String -> RewriteH LCore`	🎤 🔈
`alpha-lam`	`RewriteH LCore`	🎤 🔈
`alpha-case-binder`	`String -> RewriteH LCore`	🎤 🔈
`alpha-case-binder`	`RewriteH LCore`	🎤 🔈
`alpha-alt`	`RewriteH LCore`	🎤 🔈
`alpha-alt`	`[String] -> RewriteH LCore`	🎤 🔈
`alpha-case`	`RewriteH LCore`	🎤 🔈
`alpha-let`	`[String] -> RewriteH LCore`	🎤 🔈
`alpha-let`	`RewriteH LCore`	🎤 🔈
`alpha-top`	`[String] -> RewriteH LCore`	🎤 🔈
`alpha-top`	`RewriteH LCore`	🎤 🔈
`alpha-prog`	`RewriteH LCore`	🎤 🔈
`unshadow`	`RewriteH LCore`	🎤 🔈

`HERMIT.Dictionary.Composite`

Name	Type	Done
`unfold-basic-combinator`	`RewriteH LCore`	🎤 🔈
`simplify`	`RewriteH LCore`	🎤 🔈
`bash`	`RewriteH LCore`	🎤 🔈
`smash`	`RewriteH LCore`	🎤 🔈
`bash-extended-with`	`[RewriteH LCore] -> RewriteH LCore`	🎤 🔈
`smash-extended-with`	`[RewriteH LCore] -> RewriteH LCore`	🎤 🔈
`bash-debug`	`RewriteH LCore`	🎤 🔈

`HERMIT.Dictionary.Debug`

Name	Type	Done
`trace`	`String -> RewriteH LCoreTC`	🎤 🔈
`observe`	`String -> RewriteH LCoreTC`	🎤 🔈
`observe-failure`	`String -> RewriteH LCoreTC -> RewriteH LCoreTC`	🎤 🔈
`bracket`	`String -> RewriteH LCoreTC -> RewriteH LCoreTC`	🎤 🔈

`HERMIT.Dictionary.FixPoint`

Name	Type	Done
`fix-intro`	`RewriteH LCore`	🎤 🔈
`fix-computation-rule`	`BiRewriteH LCore`	🎤 🔈
`fix-rolling-rule`	`BiRewriteH LCore`	🎤 🔈
`fix-fusion-rule`	`String -> String -> String -> RewriteH LCore -> RewriteH LCore -> RewriteH LCore -> BiRewriteH LCore`	🎤 🔈
`fix-fusion-rule-unsafe`	`String -> String -> String -> RewriteH LCore -> BiRewriteH LCore`	🎤 🔈
`fix-fusion-rule-unsafe`	`String -> String -> String -> BiRewriteH LCore`	🎤 🔈

`HERMIT.Dictionary.Fold`

Name	Type	Done
`fold`	`HermitName -> RewriteH LCore`	🎤 🔈

`HERMIT.Dictionary.Function`

Name	Type	Done
`static-arg`	`RewriteH LCore`	🎤 🔈
`static-arg-types`	`RewriteH LCore`	🎤 🔈
`static-arg-pos`	`[Int] -> RewriteH LCore`	🎤 🔈

`HERMIT.Dictionary.GHC`

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

`HERMIT.Dictionary.Induction`

Name	Type	Done
`induction`	`HermitName -> RewriteH LCore`	🎤 🔈
`prove-by-cases`	`HermitName -> RewriteH LCore`	🎤 🔈

`HERMIT.Dictionary.Inline`

Name	Type	Done
`inline`	`RewriteH LCore`	🎤 🔈
`inline`	`OccurrenceName -> RewriteH LCore`	🎤 🔈
`inline`	`[String] -> RewriteH LCore`	🎤 🔈
`inline-case-scrutinee`	`RewriteH LCore`	🎤 🔈
`inline-case-alternative`	`RewriteH LCore`	🎤 🔈

`HERMIT.Dictionary.Kure`

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

`HERMIT.Dictionary.Local.Bind`

Name	Type	Done
`nonrec-to-rec`	`RewriteH LCore`	🎤 🔈
`rec-to-nonrec`	`RewriteH LCore`	🎤 🔈

`HERMIT.Dictionary.Local.Case`

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

`HERMIT.Dictionary.Local.Cast`

Name	Type	Done
`cast-elim`	`RewriteH LCore`	🎤 🔈
`cast-elim-refl`	`RewriteH LCore`	🎤 🔈
`cast-elim-sym`	`RewriteH LCore`	🎤 🔈
`cast-elim-sym-plus`	`RewriteH LCore`	🎤 🔈
`cast-float-app`	`RewriteH LCore`	🎤 🔈
`cast-float-lam`	`RewriteH LCore`	🎤 🔈
`cast-elim-unsafe`	`RewriteH LCore`	🎤 🔈

`HERMIT.Dictionary.Local.Let`

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

`HERMIT.Dictionary.Local`

Name	Type	Done
`beta-reduce`	`RewriteH LCore`	🎤 🔈
`beta-expand`	`RewriteH LCore`	🎤 🔈
`eta-reduce`	`RewriteH LCore`	🎤 🔈
`eta-expand`	`String -> RewriteH LCore`	🎤 🔈
`flatten-module`	`RewriteH LCore`	🎤 🔈
`flatten-program`	`RewriteH LCore`	🎤 🔈
`abstract`	`OccurrenceName -> RewriteH LCore`	🎤 🔈
`push`	`String -> RewriteH LCore -> RewriteH LCore`	🎤 🔈
`push-unsafe`	`String -> RewriteH LCore`	🎤 🔈

`HERMIT.Dictionary.Navigation.Crumbs`

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

`HERMIT.Dictionary.Navigation`

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

`HERMIT.Dictionary.New`

Name	Type	Done
`var`	`String -> TransformH LCore ()`	🎤 🔈
`nonrec-intro`	`String -> CoreString -> RewriteH LCore`	🎤 🔈

`HERMIT.Dictionary.Query`

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

`HERMIT.Dictionary.Reasoning`

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

`HERMIT.Dictionary.Remembered`

Name	Type	Done
`remember`	`LemmaName -> TransformH LCore ()`	🎤 🔈
`unfold-remembered`	`LemmaName -> RewriteH LCore`	🎤 🔈
`fold-remembered`	`LemmaName -> RewriteH LCore`	🎤 🔈
`fold-any-remembered`	`RewriteH LCore`
`show-remembered`	`PrettyPrinter -> PrettyH LCore`

`HERMIT.Dictionary.Rules`

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

`HERMIT.Dictionary.Undefined`

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

`HERMIT.Dictionary.Unfold`

Name	Type	Done
`beta-reduce-plus`	`RewriteH LCore`	🎤 🔈
`unfold`	`RewriteH LCore`	🎤 🔈
`unfold`	`OccurrenceName -> RewriteH LCore`	🎤 🔈
`unfold`	`[OccurrenceName] -> RewriteH LCore`	🎤 🔈
`unfold-saturated`	`RewriteH LCore`	🎤 🔈
`specialize`	`RewriteH LCore`	🎤 🔈
`unsafe-replace`	`CoreString -> RewriteH LCore`

`HERMIT.Dictionary.WorkerWrapper.Common`

Name	Type	Done
`intro-ww-assumption-A`		🎤 🔈
`intro-ww-assumption-B`		🎤 🔈
`intro-ww-assumption-C`		🎤 🔈
`split-1-beta`	`CoreString -> RewriteH LCore`	🎤 🔈
`split-2-beta`	`CoreString -> RewriteH LCore`	🎤 🔈

`HERMIT.Dictionary.WorkerWrapper.Fix`

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

`HERMIT.Dictionary.WorkerWrapper.FixResult`

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

`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`	🎤 🔈
`abort`	`ShellEffect`	🎤 🔈
`continue`	`ShellEffect`	🎤 🔈
`gc`
`gc`
`display`		🎤 🔈
`up`	`KernelEffect`	🎤 🔈
`navigate`
`command-line`
`set-window`	`ShellEffect`	🎤 🔈
`top`	`KernelEffect`	🎤 🔈
`log`	`QueryFun`	🎤 🔈
`back`	`ShellEffect`	🎤 🔈
`step`	`ShellEffect`	🎤 🔈
`goto`
`goto`
`tag`	`String -> ShellEffect`	🎤 🔈
`diff`	`AST -> AST -> QueryFun`	🎤 🔈
`set-pp-diffonly`	`Bool -> ShellEffect`	🎤 🔈
`set-fail-hard`	`Bool -> ShellEffect`	🎤 🔈
`set-auto-corelint`	`Bool -> ShellEffect`	🎤 🔈
`set-pp`	`String -> ShellEffect`	🎤 🔈
`set-pp-renderer`
`set-pp-renderer`
`dump`
`dump`
~~`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`	🎤 🔈
`set-pp-type`	`PpType -> ShellEffect`	🎤 🔈
`set-pp-coercion`	`PpType -> ShellEffect`	🎤 🔈
`set-pp-uniques`	`Bool -> ShellEffect`	🎤 🔈
`{`	`KernelEffect`	🎤 🔈
`}`	`KernelEffect`	🎤 🔈
`load`	`String -> String -> ScriptEffect`	🎤 🔈
`load-and-run`	`String -> ScriptEffect`	🎤 🔈
`save`	`String -> ScriptEffect`	🎤 🔈
`save-verbose`	`String -> ScriptEffect`	🎤 🔈
`save-script`	`String -> String -> ScriptEffect`	🎤 🔈
`load-as-rewrite`	`String -> String -> ScriptEffect`	🎤 🔈
`script-to-rewrite`		🎤 🔈
`define-script`		🎤 🔈
`define-rewrite`		🎤 🔈
`run-script`		🎤 🔈
`display-scripts`		🎤 🔈
`stop-script`		🎤 🔈
`possible-rewrites`	`CommandLineState -> TransformH LCore String`

`HERMIT.Shell.Proof`

Name	Type	Done
`prove-lemma`	`LemmaName -> ShellEffect`	🎤 🔈
`end-proof`	`ProofShellCommand`	🎤 🔈
`end-case`	`ProofShellCommand`	🎤 🔈
`assume`	`ProofShellCommand`	🎤 🔈

HERMIT to HERMIT Shell

Symbols

Types

All shell functions

Clone this wiki locally