Skip to content


Here are 175 public repositories matching this topic...

CohenCyril commented Nov 2, 2020

Description of the problem

The following code does not raise an error, and the behavior is undocumented.

Section Test.
Variables (b : bool) (n : nat) (All : unit).
Collection n := b.

Lemma foo : True.
Proof using n.

Lemma bar : True.
Proof using All.
End Test.

Check foo : bool -> True.
Check bar : bool -> nat -> unit -> True.
mtzguido commented Oct 8, 2018

This is very low prio, but it usually happens that when touching Prims or some other file high in the dependency graph, we get spurious diffs in many other files. Since we check-in the snapshot, and we need to have it up-to-date, we get very verbose commits when nothing relevant changed. Plus, when something did change, it's hard to spot.

Example: I removed a few lines in prims and get things

astump commented Jan 15, 2020

It would be a nice convenience to allow the syntax

import M as _.

This would have the effect of checking module M but not adding any of its names to the context of the importing file. The use case for this is if you want to have a single Cedille source file that includes a bunch of other files, without having to worry about namespace clashes. This would be handy for testing. One can achie

fblanqui commented Feb 23, 2019

This issue is not urgent. I open it to keep it in mind.

Many tools use now for their doc, including Coq. See . It seems to be automatically generated from html and files in

Perhaps we should do the same to get a better rendering of the doc.

Improve this page

Add a description, image, and links to the dependent-types topic page so that developers can more easily learn about it.

Curate this topic

Add this topic to your repo

To associate your repository with the dependent-types topic, visit your repo's landing page and select "manage topics."

Learn more

You can’t perform that action at this time.