CurryInfo: verify-non-fail-2.0.0 / Verify.ESMT.rnmQIdWithTInstTerm

 
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)

 argument 2

 deterministic operation

 
Rename all sorted names occurring in a term w.r.t. its type instance
of the polymorphic function.

 <FAILING>

 referentially transparent operation

 no fixity defined

 {(_,{TConst}) |-> {TConst} || (_,{TSVar}) |-> {TSVar} || (_,{TComb}) |-> {TComb} || (_,{Forall}) |-> {Forall} || (_,{Exists}) |-> {Exists} || (_,{Let}) |-> {Let} || (_,{Match}) |-> {Match}}

 rnmQIdWithTInstTerm

 no precedence defined

 _

 [(String, ([String], Sort))] -> Term -> Term

 operation might suspend on free variables

 possibly non-terminating

 possibly non-reducible on same data term