this fib code should work

[bizid777]

divergent def fib (n : U32) : Result U32 :=
match n with
| 0#scalar => Result.ok 1#u32
| 1#scalar => Result.ok 1#u32
| _ =>
do
let i ← n - 1#u32
let i1 ← fib i
let i2 ← n - 2#u32
let i3 ← fib i2
i1 + i3

end aeneas_test

[sonmarcho]

Could you please precise what the exact issue is? The model doesn't type-check (with what error message)?

[bizid777]

the Leaninfoview shows this error: application type mismatch match n with | { val := 0, hmin := hmin, hmax := hmax } => Aeneas.Diverge.FixII.is_valid_p_same k.3 (Result.ok 1#u32) | { val := 1, hmin := hmin, hmax := hmax } => Aeneas.Diverge.FixII.is_valid_p_same k.3 (Result.ok 1#u32) | x => Aeneas.Diverge.FixII.is_valid_p_bind (Aeneas.Diverge.FixII.is_valid_p_same k.3 (n - 1#u32)) fun i => Aeneas.Diverge.FixII.is_valid_p_bind (Aeneas.Diverge.FixII.is_valid_p_rec k.3 (Fin.ofNat 0) PUnit.unit i) fun i1 => Aeneas.Diverge.FixII.is_valid_p_bind (Aeneas.Diverge.FixII.is_valid_p_same k.3 (n - 2#u32)) fun i2 => Aeneas.Diverge.FixII.is_valid_p_bind (Aeneas.Diverge.FixII.is_valid_p_rec k.3 (Fin.ofNat 0) PUnit.unit i2) fun i3 => Aeneas.Diverge.FixII.is_valid_p_same k.3 (i1 + i3) argument fun x => Aeneas.Diverge.FixII.is_valid_p_bind (Aeneas.Diverge.FixII.is_valid_p_same k.3 (n - 1#u32)) fun i => Aeneas.Diverge.FixII.is_valid_p_bind (Aeneas.Diverge.FixII.is_valid_p_rec k.3 (Fin.ofNat 0) PUnit.unit i) fun i1 => Aeneas.Diverge.FixII.is_valid_p_bind (Aeneas.Diverge.FixII.is_valid_p_same k.3 (n - 2#u32)) fun i2 => Aeneas.Diverge.FixII.is_valid_p_bind (Aeneas.Diverge.FixII.is_valid_p_rec k.3 (Fin.ofNat 0) PUnit.unit i2) fun i3 => Aeneas.Diverge.FixII.is_valid_p_same k.3 (i1 + i3) has type U32 → Aeneas.Diverge.FixII.is_valid_p k.3 fun k => do let y ← n - 1#u32 let y ← k (Fin.ofNat 0) PUnit.unit y let y_1 ← n - 2#u32 let y_2 ← k (Fin.ofNat 0) PUnit.unit y_1 y + y_2 : Prop but is expected to have type ∀ (x : U32), Aeneas.Diverge.FixII.is_valid_p k.3 fun kk.2 => match x with | { val := 0, hmin := hmin, hmax := hmax } => Result.ok 1#u32 | { val := 1, hmin := hmin, hmax := hmax } => Result.ok 1#u32 | x => do let i ← n - 1#u32 let i1 ← kk.2 (Fin.ofNat 0) PUnit.unit i let i2 ← n - 2#u32 let i3 ← kk.2 (Fin.ofNat 0) PUnit.unit i2 i1 + i3 : Prop

…

________________________________ From: Son HO ***@***.***> Sent: Monday, January 27, 2025 13:30 To: AeneasVerif/aeneas ***@***.***> Cc: Adem Bizid ***@***.***>; Author ***@***.***> Subject: Re: [AeneasVerif/aeneas] this fib code should work (Issue #425) Could you please precise what the exact issue is? The model doesn't type-check (with what error message)? — Reply to this email directly, view it on GitHub<#425 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/BM72VVU3BBAPWZ3YSL2KVDD2MZ3MDAVCNFSM6AAAAABV6WA5XKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDMMJWGU4DQMRRGM>. You are receiving this because you authored the thread.Message ID: ***@***.***>