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	LemmaName -> LemmaName -> LemmaName -> Transform LCore ()	🎤 🔈
disjunct	LemmaName -> LemmaName -> LemmaName -> Transform LCore ()	🎤 🔈
imply	LemmaName -> LemmaName -> LemmaName -> Transform 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	LemmaName -> HermitName -> CoreString -> 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	🎤 🔈

HERMIT.Dictionary.Unsafe

Name	Type	Done
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	String -> String -> BiRewriteH LCore	🎤 🔈
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	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	🎤 🔈
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	✅