juvix/tests/negative/Internal/WrongConstructorArity.juvix

module WrongConstructorArity;

type T :=
  | A : T → T;

f : T → T
  | (A i x) := i;
[typecheck] Shortcircuit clause pattern check errors In the following case: ``` module WrongConstructorArity; inductive T { A : T; }; f : T → T; f (A i) ≔ i; end; ``` The typechecker fails when checking the clause `f (A i) := i` because of the extra constructor argument. However if typechecking continues then the variable `i` on the rhs does not have a type so we must short-circuit. 2022-04-08 12:26:20 +03:00			`module WrongConstructorArity;`

Fix Makefile target bugs for formatting and type Checking Juvix files (#2057) This PR resolves a few bugs in the Makefile targets for formatting and type checking Juvix files, which were preventing the capture of type checking errors for our examples and bad formatting for all the Juvix files in the repository. With this PR, our code should now be clean, and we can expect every file to be properly formatted and type checked. Changes made: - [x] Updated `make format-juvix-files` - [x] Updated `make check-format-juvix-files` - [x] Formatted all Juvix files - [x] Comment a fragment in `examples/milestone/Bank/Bank.juvix` In the future, we will drastically simplify the Makefile once we improve the `format` and the `type check` command for example posted here: - #2066 - #2087 Related: - #2063 - #2040 (due to some typechecking errors we're not capturing before) - #2105 - https://github.com/anoma/juvix/issues/2059 2023-05-19 18:33:56 +03:00			`type T :=`
			`\| A : T → T;`

Format juvix files using new function syntax (#2245) 2023-07-11 18:22:07 +03:00			`f : T → T`
			`\| (A i x) := i;`