lean
import SFLean4.LF.Imp《软件基础》卷二 (PLF) - Imp 命令式语言桥接 (Imp)
本模块直接继承并再导出卷一 SFLean4.LF.Imp 中定义的简单命令式语言 Imp， 包括算术表达式 aexp、布尔表达式 bexp、命令语法 com 以及大步操作语义 ceval。
lean
namespace PLF
open Imp
end PLF