Pantograph/Test/Common.lean

21 lines
352 B
Plaintext
Raw Permalink Normal View History

import Pantograph.Protocol
namespace Pantograph
namespace Protocol
/-- Set internal names to "" -/
def Goal.devolatilize (goal: Goal): Goal :=
{
goal with
2023-10-30 14:44:06 -07:00
name := "",
vars := goal.vars.map removeInternalAux,
}
where removeInternalAux (v: Variable): Variable :=
{
v with
name := ""
}
end Protocol
end Pantograph