diff --git a/tests/lean/run/1089.lean b/tests/lean/run/1089.lean new file mode 100644 index 0000000000..cede2af532 --- /dev/null +++ b/tests/lean/run/1089.lean @@ -0,0 +1,21 @@ +import init.string +import init.bool +import system.io + +inductive token +| eof : token +| plus : token +| var : string -> token + +open token +open option + +def to_token : string → option token +| [] := none +| (c :: cs) := + let t : option token := match c with + | #"x" := some (var "x") + | #"y" := some (var "y") + | #"+" := some plus + | _ := none + end in t