lean2/tests/lean/run/t11.lean

constant A : Type.{1}
constants a b c : A
constant f : A → A → A
check f a b
section
  parameters A B : Type
  parameters {C D : Type}
  parameters [e : A] [d : A]
  check A
  check B
  definition g (a : A) (b : B) (c : C) : A := e
end
check g.{2 1}
constants x y : A
refactor(frontends/lean): constant/axiom are top-level commands, parameter/variable/hypothesis/conjecture are section/context-level commands Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-10-02 23:20:52 +00:00			`constant A : Type.{1}`
			`constants a b c : A`
			`constant f : A → A → A`
feat(frontends/lean/builtin_cmds): add 'variables' command family Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-06-17 15:25:00 +00:00			`check f a b`
chore(tests): remove most occurrences of 'context' command from the test suite 2015-04-22 02:33:21 +00:00			`section`
feat(frontends/lean/builtin_cmds): change notation for marking implicit/cast parameter in sections Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-06-23 00:51:00 +00:00			`parameters A B : Type`
			`parameters {C D : Type}`
feat(frontends/lean): automatically include anonymous instance implicit variables/parameters (whenever their parameters have been included) 2015-12-13 21:20:07 +00:00			`parameters [e : A] [d : A]`
feat(frontends/lean/builtin_cmds): add 'variables' command family Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-06-17 15:25:00 +00:00			`check A`
			`check B`
			`definition g (a : A) (b : B) (c : C) : A := e`
			`end`
			`check g.{2 1}`
refactor(frontends/lean): constant/axiom are top-level commands, parameter/variable/hypothesis/conjecture are section/context-level commands Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-10-02 23:20:52 +00:00			`constants x y : A`