lean2/tests/lean/abbrev2.lean.expected.out

17 lines
324 B
Text
Raw Permalink Normal View History

definition bla.tst :
foo
definition bla.tst :
10 + 1
abbrev2.lean:12:6: error: unknown identifier 'bla.foo'
abbrev2.lean:14:6: error: unknown identifier 'foo'
definition bla.tst :
10 + 1
definition bla2.tst2 :
foo2
definition bla2.tst2 :
1
definition bla2.tst2 :
foo2
definition bla2.tst2 :
foo2