Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

ceta should export nat_of_integer #21

Open
jwaldmann opened this issue Jun 28, 2020 · 3 comments
Open

ceta should export nat_of_integer #21

jwaldmann opened this issue Jun 28, 2020 · 3 comments

Comments

@jwaldmann
Copy link
Owner

my main program does import Ceta to call

certify_proof ::
  Bool ->
    Maybe [Char] ->
      Sum (Claim (Lab [Char] [Nat]) [Char]) [Char] -> [Char] -> Cert_result;

We have

data Claim a b = Yes | No | Terminating | Upperbound Nat | Nonterminating
  | Confluent | Nonconfluent | Completed | Ordered_Completed | Anything;

but

module
  Ceta(Nat,

so I cannot construct Upperbound Nat.

(see #19 )

@jwaldmann
Copy link
Owner Author

I can fix this manually for now (just add the export) but it's not stable.

@jwaldmann
Copy link
Owner Author

the commit is the work-around, I keep the issue open.

@jwaldmann jwaldmann reopened this Jun 28, 2020
@csternagel
Copy link

With changeset f1285556fa56 of IsaFor ( http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR ) nat_of_integer is now exported by Ceta.hs.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants