dependent-types

Code like

have {H}H : ...

triggers a cryptic warning. It should suggest to write

have {}H : ...

instead.

See also: https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/duplicate.20clear

Describe the bug

When installing the Kind toolchain the kind-scm command is installed. When I read [THEOREMS.md][theorems] the command is named kind.

To Reproduce

Steps to reproduce the behavior:

1. Following installation instructions for Ubuntu
2. Read [THEOREMS.md][theorems]

Expected behavior

I would expect

A formula like forall x1. forall. x2. exists x3. phi gets resugared to, and hence pretty printed as, forall x1 x2 x3. phi. The bug is in the uncurry function in FStar.Syntax.Reguar.fs.

unwords, unlines, etc. have ad-hoc implementations that should be refactored via

join : String -> List String -> String
join sep ws = concat (intersperse sep ws)

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