diff options
Diffstat (limited to 'backends/lean/Base/Diverge/Base.lean')
| -rw-r--r-- | backends/lean/Base/Diverge/Base.lean | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean index a7107c1e..bdc3ed04 100644 --- a/backends/lean/Base/Diverge/Base.lean +++ b/backends/lean/Base/Diverge/Base.lean @@ -5,6 +5,7 @@ import Mathlib.Tactic.RunCmd import Mathlib.Tactic.Linarith import Base.Primitives.Base import Base.Arith.Base +import Base.Diverge.ElabBase /- TODO: this is very useful, but is there more? -/ set_option profiler true @@ -1467,6 +1468,7 @@ namespace Ex8 .ret (hd :: tl) /- The validity theorem for `map`, generic in `f` -/ + @[divspec] theorem map_is_valid (i : id) (t : ty i) {{f : (a i t → Result (b i t)) → (a i t) → Result c}} @@ -1479,6 +1481,7 @@ namespace Ex8 intros apply is_valid_p_bind <;> try simp_all + @[divspec] theorem map_is_valid' (i : id) (t : ty i) (k : ((i:id) → (t:ty i) → a i t → Result (b i t)) → (i:id) → (t:ty i) → a i t → Result (b i t)) |