Pedro Abreu

Translate Coq recursion that does not directly pattern matches

2

Cedille recursion is tied with recursion, which is not necessarily the case with Coq. This brings us to the question of how to deal functions like `f` bellow. ``` Fixpoint...

Cedille does not accept names to start with an underscore. Check `Coq.Init.Logic.neg_false` for an example of where this causes a failure.

Add a new variable to the environent `fresh_ctx := alist Ced.Var nat` that will count the number of occurrences of a variable in the term, now the fresh variable generator...

Cast Recursive Argument Constructor Arguments when necessary

1

Consider `le_ind`, it is currently translated this way: ``` le_ind : Π n : nat . ∀ P : nat ➔ ★ . Π f : P n . Π...

Consider the (failing) translation of ex_ind ``` data ex (A : ★) (P : A ➔ ★) : ★ = | ex_intro : Π x : A . P x...

Wrap new lines on char count = 80

In term level type annotations are unnecessary. This is a feature request to implement a flag to turn them on and off on request.

Using the internals provided by the Hearthstone Deck Tracker it was possible to retrieve the card automaticaly, without the need to run through every card in the collections. Closes #67...

It would cause compilation warnings, removing them will make compilation smoother.