format-id error: given: #<syntax (even n)>

[sorawee]

I'm translating Coq's even_plus_even_is_even to cur.

Inductive even : nat -> Set :=
  | even_O : even O
  | even_SSn : forall n:nat,
                even n -> even (S (S n)).
 
 
Theorem even_plus_even_is_even : forall n m : nat,
  even n -> even m -> even (n + m).
Proof.
  intros n m Hn Hm.

  induction Hn as [|n' IHn].
  - simpl.
    assumption.

  - simpl.
    apply even_SSn.
    assumption.
Qed.

In cur, I am at this step:

(data even : 0 (-> nat Type)
      [even-O : (even 0)]
      [even-SS : (forall [n : nat] (-> (even n) (even (S (S n)))))])

(define-theorem even-plus-even-is-even
  (∀ [n : nat] [m : nat] (-> (even n) (even m) (even (+ n m))))
  (by-intros n m Hn Hm)
  
  display-focus
  
  (by-induction Hn #:as [() (n* IHn)]))

display-focus seems to show that I'm heading in the right direction. However, by-induction on Hn: (even n) results in:

format-id: contract violation
  expected: (or/c string? symbol? identifier? keyword? char? number?)
  given: #<syntax (even n)>

[wilbowma]

Are you working from master?

…

-- Sent from my phoneamajig

On Aug 27, 2019, at 20:08, sorawee ***@***.***> wrote: I'm translating Coq's even_plus_even_is_even to cur. Inductive even : nat -> Set := | even_O : even O | even_SSn : forall n:nat, even n -> even (S (S n)). Theorem even_plus_even_is_even : forall n m : nat, even n -> even m -> even (n + m). Proof. intros n m Hn Hm. induction Hn as [|n' IHn]. - simpl. assumption. - simpl. apply even_SSn. assumption. Qed. In cur, I am at this step: (data even : 0 (-> nat Type) [even-O : (even 0)] [even-SS : (forall [n : nat] (-> (even n) (even (S (S n)))))]) (define-theorem even-plus-even-is-even (∀ [n : nat] [m : nat] (-> (even n) (even m) (even (+ n m)))) (by-intros n m Hn Hm) display-focus (by-induction Hn #:as [() (n* IHn)])) display-focus seems to show that I'm heading in the right direction. However, by-induction on Hn: (even n) results in: format-id: contract violation expected: (or/c string? symbol? identifier? keyword? char? number?) given: #<syntax (even n)> — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or mute the thread.

[sorawee]

I raco pkg install cur. I think that is master.

[wilbowma]

Yeah it is. We're in the middle of a massive rewrite; if you're up to experimenting, you can try the "turnstile-core" branch. The tactics are much improved, among other things. But the are still bugs, and it's not easy to back port fixes. I'll see if I can debug your issue later this week.

…

-- Sent from my phoneamajig

On Aug 27, 2019, at 20:13, sorawee ***@***.***> wrote: I raco pkg install cur. I think that is master. — You are receiving this because you commented. Reply to this email directly, view it on GitHub, or mute the thread.

[stchang]

The added test seems to be equivalent to the example, and does not error.

Re-open if there is still a problem