coquedille

coquedille copied to clipboard

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...

pedrotst

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.

pedrotst

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...

pedrotst

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 . Π...

pedrotst

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

pedrotst

Wrap new lines on char count = 80

pedrotst

Fix identation for nested pattern matching / recursion

1

pedrotst

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

pedrotst