Diverge.lean « Base « lean « backends - aeneas - aeneas rust verifier with a hacky Isabelle backend

summary refs log tree commit diff

path: root/backends/lean/Base/Diverge.lean

blob: 92ffd3cdbe80b98afb0bf267c6a416bc661c0e13 (plain)

import Lean
import Lean.Meta.Tactic.Simp
import Init.Data.List.Basic
import Mathlib.Tactic.Linarith
import Base.Diverge.Base
import Base.Diverge.Elab