proofs/NectarDriver/Impl.v


1
2
3
4
5
6
7
8
9
10
11

(*
    NectarDriver: Impl keyword.

    The Impl keyword defines methods and/or traits associated with a specific identifier N.

    Author: Amlal El Mahrouss
    Formalization: January 2026
*)

Require Import Logic.Classical_Prop.
Require Import NectarDriver.Traits.