Why3
1 program
Added 2025-11-05T12:01:43Z
Model: x-ai/grok-4-fastTemp: 0.4
Evidence
Report issue
View issues
Aliases: —
Provenance: commit 9ffcf62e3d · authored 2025-11-05T13:01:43+01:00 · model x-ai/grok-4-fast
Sources mentioning this language
1 source · not in taxonomy (canonical name didn't match any upstream)
Related languages
LLM-contributed programs
Introductory Why3 Example
Provenance: commit 9ffcf62e3d · authored 2025-11-05T13:01:43+01:00 · model x-ai/grok-4-fast · Temp 0.4
(*
This file is part of the Why3 platform, distributed under the terms
of the Lesser General Public License version 2.1, with the special
clause on the linking of executable modules.
Copyright (C) 2009-2023 CNRS
Jean-Christophe Filliâtre (filliatre@lri.fr)
François Bobot (bobot@lri.fr)
Claude Marché (marché@lri.fr)
Guillaume Melquiond (melquiond@lri.fr)
Andrei Paskevich (paskevich@lri.fr)
*)
module Intro
use import int.Int
let even (n:int) : bool = n mod 2 = 0
goal G1: forall n:int. even n <-> n mod 2 = 0
intros n. unfold even. reflexivity. qed
goal G2: forall n:int. even (n + 2) <-> even n
intros n. unfold even. rewrite (plus_remainder n 2). ring. qed
end