diff options
| author | Josh Chen | 2021-01-18 23:49:13 +0000 |
|---|---|---|
| committer | Josh Chen | 2021-01-18 23:49:13 +0000 |
| commit | f46df86db9308dde29e0e5f97f54546ea1dc34bf (patch) | |
| tree | b9523698c4ec81f3bba8f6b549d386505e345746 /spartan/core/rewrite.ML | |
| parent | 3922e24270518be67192ad6928bb839132c74c07 (diff) | |
Swapped notation for metas (now ?) and holes (now {}), other notation and name changes.
Diffstat (limited to 'spartan/core/rewrite.ML')
| -rw-r--r-- | spartan/core/rewrite.ML | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/spartan/core/rewrite.ML b/spartan/core/rewrite.ML index 99c21b5..af70cfc 100644 --- a/spartan/core/rewrite.ML +++ b/spartan/core/rewrite.ML @@ -72,13 +72,13 @@ fun mk_hole i T = Var ((holeN, i), T) fun is_hole (Var ((name, _), _)) = (name = holeN) | is_hole _ = false -fun is_hole_const (Const (\<^const_name>\<open>rewrite_HOLE\<close>, _)) = true +fun is_hole_const (Const (\<^const_name>\<open>rewrite_hole\<close>, _)) = true | is_hole_const _ = false val hole_syntax = let (* Modified variant of Term.replace_hole *) - fun replace_hole Ts (Const (\<^const_name>\<open>rewrite_HOLE\<close>, T)) i = + fun replace_hole Ts (Const (\<^const_name>\<open>rewrite_hole\<close>, T)) i = (list_comb (mk_hole i (Ts ---> T), map_range Bound (length Ts)), i + 1) | replace_hole Ts (Abs (x, T, t)) i = let val (t', i') = replace_hole (T :: Ts) t i |