|
definition:
|
rnmQIdWithTInstTerm :: [(Ident, ([Ident],Sort))] -> Term -> Term
rnmQIdWithTInstTerm sigs term = case term of
TConst _ -> term
TSVar _ -> term
TComb f args -> TComb (rnmQIdWithTInst sigs f)
(map (rnmQIdWithTInstTerm sigs) args)
Forall svs arg -> Forall svs (rnmQIdWithTInstTerm sigs arg)
Exists svs arg -> Exists svs (rnmQIdWithTInstTerm sigs arg)
Let bs e -> Let (map (\ (v,s) -> (v, rnmQIdWithTInstTerm sigs s)) bs)
(rnmQIdWithTInstTerm sigs e)
Match e ps -> Match (rnmQIdWithTInstTerm sigs e)
(map (\ (v,s) -> (v, rnmQIdWithTInstTerm sigs s)) ps)
|
|
demand:
|
argument 2
|
|
deterministic:
|
deterministic operation
|
|
documentation:
|
Rename all sorted names occurring in a term w.r.t. its type instance
of the polymorphic function.
|
|
failfree:
|
<FAILING>
|
|
indeterministic:
|
referentially transparent operation
|
|
infix:
|
no fixity defined
|
|
iotype:
|
{(_,{TConst}) |-> {TConst} || (_,{TSVar}) |-> {TSVar} || (_,{TComb}) |-> {TComb} || (_,{Forall}) |-> {Forall} || (_,{Exists}) |-> {Exists} || (_,{Let}) |-> {Let} || (_,{Match}) |-> {Match}}
|
|
name:
|
rnmQIdWithTInstTerm
|
|
precedence:
|
no precedence defined
|
|
result-values:
|
_
|
|
signature:
|
[(String, ([String], Sort))] -> Term -> Term
|
|
solution-complete:
|
operation might suspend on free variables
|
|
terminating:
|
possibly non-terminating
|
|
totally-defined:
|
possibly non-reducible on same data term
|