Google Git Google Git
Sign in
fuchsia/third_party/github.com/leanprover/lean4/refs/heads/upstream/replace/./tests/lean/mvarAtDefaultValue.lean.expected.out
blob: 1d624efc9b4a65cb55bf953d6f16e2781f0715c0 [file] [edit]
mvarAtDefaultValue.lean:5:2-5:3: error: invalid default value for field, it contains metavariables
?m
mvarAtDefaultValue.lean:8:2-8:3: error: invalid default value for field, it contains metavariables
?m + 1