From d9101cb950d980d1853c3015594d6bf681ba2ed4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 2 May 2018 17:37:55 -0700 Subject: [PATCH] chore(tests/lean/parser1): fix test --- tests/lean/parser1.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/tests/lean/parser1.lean b/tests/lean/parser1.lean index d153bff7ab..cbaeb088d9 100644 --- a/tests/lean/parser1.lean +++ b/tests/lean/parser1.lean @@ -111,7 +111,6 @@ do cmd ← lean.ir.parse_instr, #eval test parse_instr_pp "o := cnstr 0 3 0" "o := cnstr 0 3 0" #eval test parse_instr_pp "set o 0 x" "set o 0 x" #eval test parse_instr_pp "x := get o 0" "x := get o 0" -#eval test parse_instr_pp "«set» := get o 0" "«set» := get o 0" #eval test parse_instr_pp "sset o 10 x" "sset o 10 x" #eval test parse_instr_pp "x : bool := sget o 0" "x : bool := sget o 0" #eval test parse_instr_pp "x := closure f a" "x := closure f a"