From f84ea289234e40c26f482b8715e72d7ad31e3ac4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 21 May 2019 08:11:48 -0700 Subject: [PATCH] fix(library/init/lean/compiler/ir/emitutil): missing `FnBody.case` --- library/init/lean/compiler/ir/emitutil.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/library/init/lean/compiler/ir/emitutil.lean b/library/init/lean/compiler/ir/emitutil.lean index 3809c291b7..a01fb15029 100644 --- a/library/init/lean/compiler/ir/emitutil.lean +++ b/library/init/lean/compiler/ir/emitutil.lean @@ -92,6 +92,7 @@ local infix ` >> `:50 := Function.comp partial def collectFnBody : FnBody → Collector | (FnBody.vdecl x t _ b) := collectVar x t >> collectFnBody b | (FnBody.jdecl j xs v b) := collectJP j xs >> collectParams xs >> collectFnBody v >> collectFnBody b +| (FnBody.case _ _ alts) := λ s, alts.foldl (λ s alt, collectFnBody alt.body s) s | e := if e.isTerminal then id else collectFnBody e.body def collectDecl : Decl → Collector