Rígille S. B. Menezes

### Describe the bug Sometimes a datatype declaration isn't expanded to a well-typed term. ### To Reproduce ``` type PriorityQueue.Tree { empty node(rank: Nat, element: A, left: PriorityQueue.Tree, right: PriorityQueue.Tree)...

### Describe the bug Sometimes the smart motive doesn't make all the substitutions it should and that results in confusing error messages. ### To Reproduce Copy and paste the following...

using Parser blocks as local variables fails in compilation

1

when Kind is compiled to FormCore, it inlines certain definitions, such as Parser.bind and Parser.pure. because of that, if you use "let" to define a parser, such as: ``` Test:...

equivalent redefinition of Bool changes results

2

# expected behavior in the program ``` type Bool { false true } Bool.and(x: Bool, y: Bool): Bool case x { false: Bool.false true: y } Test: _ Bool.show(Bool.and(Bool.true, Bool.false))...

# expected behavior given the program ```js type Subset ~ (A: Type) { nat ~ (A = Nat) str ~ (A = String) } DummyFn(x: A): A x Test: Nat...

Typing ``` 0 \not\in \mathbb{N} ``` I expected to get ``` 0 ∉ ℕ ``` Instead I got ``` 0 ̸∈ ℕ ``` and ``` 0 \in\not \mathbb{N} ``` yields...

Allow svgs to be transformed

1

I see there's this TODO in `svg/src/lib.rs`: ``` // TODO(pcwalton): Allow a global transform to be set. ``` If I made a PR for this, would anyone be available to...