remove redundant check

[HuStmpHrrr]

Closes #252

[HuStmpHrrr]

current extraction:

(** val read_nf_impl : nat -> domain_nf -> nf **)

let rec read_nf_impl s = function
| D_dom (d0, d1) ->
  (match d0 with
   | D_nat ->
     (match d1 with
      | D_zero -> Nf_zero
      | D_succ d2 -> Nf_succ (read_nf_impl s (D_dom (D_nat, d2)))
      | D_neut (_, d2) -> Nf_neut (read_ne_impl s d2)
      | _ -> assert false (* absurd case *))
| ...

the type annotation is safe to ignore for the neutral case.

[Ailrun]

Other than the above comment, LGTM.

[HuStmpHrrr]

Not sure. Does it do u shelve? I don't even know when this unresolved goal is coming from. Thanks, Jason Hu

…

________________________________ From: Ailrun ***@***.***> Sent: Wednesday, October 16, 2024 4:49:09 PM To: Beluga-lang/McLTT ***@***.***> Cc: Jason Hu ***@***.***>; Author ***@***.***> Subject: Re: [Beluga-lang/McLTT] remove redundant check (PR #253) @Ailrun approved this pull request. Other than the above comment, LGTM. — Reply to this email directly, view it on GitHub<#253 (review)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/ABORVT6SK5UJAEBV6CGS4KLZ33GMLAVCNFSM6AAAAABQCHNL3SVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMZDGNZTGY2TINJZGY>. You are receiving this because you authored the thread.Message ID: ***@***.***>

[Ailrun]

It solves shelved goals as well, so it should work if it is generated because of the universe of Nat.

[HuStmpHrrr]

it's not really about universe levels. It asks for a domain. I am not sure which lemma it's coming from, but is definitely caused by my change. but in any case, mautosolve does handle it.