Commit graph

2 commits

Author SHA1 Message Date
Leonardo de Moura
8df7c7b02d feat(kernel/type_checker): remove fallback that expands opaque definitions in the type checker
We should not rely on this feature. It can be quite expensive.
We invoke is_convertible in several places, in particular, if we are using overloading. For example, the frontend uses is_convertible to check which overload should be used. Thus, it will make several calls such as

   is_convertible(num, Nat)

If is_convertible starts unfolding opaque definitions, we would keep expanding num.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-09 11:31:24 -08:00
Leonardo de Moura
593f1f2ebd fix(frontends/lean): allow user set constants defined in other namespaces as opaque
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 20:56:31 -08:00