From 7ec0505e94017d31b84510a0752acc30911dfcea Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 25 Feb 2017 12:47:58 -0800 Subject: [PATCH] chore(library/init/meta/vm): style --- library/init/meta/vm.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/init/meta/vm.lean b/library/init/meta/vm.lean index 8c98d571ef..32041bf555 100644 --- a/library/init/meta/vm.lean +++ b/library/init/meta/vm.lean @@ -130,8 +130,8 @@ do fmt ← return $ to_fmt a, end vm -meta structure vm_monitor (s : Type) := -(init : s) (step : s → vm s) +meta structure vm_monitor (α : Type) := +(init : α) (step : α → vm α) /- Registers a new virtual machine monitor. The argument must be the name of a definition of type `vm_monitor S`. The command will override the last monitor.