Mentions légales du service

Skip to content

Add a transformation "extensionality" to help with proofs of equality.

Adding meta extensionality function byte'int to the following file makes Alt-Ergo go from 22 to 16 steps:

use mach.int.Byte
let foo (x : byte) ensures { result = x } = x + 0

Adding meta extensionality predicate Seq.(==) to the following file makes Alt-Ergo go from timeout to instant:

use int.Int
use seq.Seq

let foo () =
  let s1 = create 5 (fun i -> i) in
  let s2 = create 5 (fun i -> i + 0) in
  assert { s1 = s2 }

Merge request reports

Loading