Skip to content

Cannot redefine bool and tt #392

@FissoreD

Description

@FissoreD

Not sure whether this is a real bug, but I would like to define a
self-contained program, i.e., without relying on the ELPI standard library.
I would like to redefine the bool type with its constructors.

The file looks like:

% main.elpi
kind bool type.
type tt bool.    % The error is at this line
type ff bool.

However, when I execute the command elpi main.elpi -test, I get the
following error:

Incompatible provenance for symbol ff: Ast.Structured.Elpi !=
(Ast.Structured.OCaml Ast.Structured.Builtin {variant = 1})

Is this expected, or should the compiler understand that adding
tt to bool is a no-op, since tt already exists as
a constructor of bool in the standard library?

Moreover, what I find weird is that I can create type tt int -> bool without warnings

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions