@@ -0,0 +1,26 @@
1+import Language.Reflection.Utils
2+import Pruviloj.Core
3+
4+forgotToNatAndRename : TTName -> TTName -> Raw -> Raw
5+forgotToNatAndRename old new (RBind name b body) = RBind name (map (forgotToNatAndRename old new) b) (forgotToNatAndRename old new body)
6+forgotToNatAndRename old new (RApp f arg) = RApp (forgotToNatAndRename old new f) (forgotToNatAndRename old new arg)
7+forgotToNatAndRename old new (RConstant Forgot) = Var `{Nat}
8+forgotToNatAndRename old new (Var n) = if n == old then Var new else Var n
9+forgotToNatAndRename old new tm = tm
10+
11+roundtrip : TTName -> TTName -> Elab ()
12+roundtrip old new = do
13+ DefineFun _ clauses <- lookupFunDefnExact old
14+ clauses' <- for clauses (\(MkFunClause lhs rhs) => do
15+ lhs' <- forgotToNatAndRename old new <$> forget lhs
16+ rhs' <- forgotToNatAndRename old new <$> forget rhs
17+ pure $ MkFunClause lhs' rhs')
18+ defineFunction (DefineFun new clauses')
19+
20+plus' : Nat -> Nat -> Nat
21+%runElab (roundtrip `{plus} `{plus'})
22+
23+total
24+p : (a : Nat) -> (b : Nat) -> plus a b = plus' a b
25+p Z right = Refl
26+p (S left) right = Refl