diff options
| author | Amlal El Mahrouss <amlal@nekernel.org> | 2026-01-26 02:56:49 +0100 |
|---|---|---|
| committer | Amlal El Mahrouss <amlal@nekernel.org> | 2026-01-26 02:56:49 +0100 |
| commit | 583b55feacdb641bb467c6ad8c3a790185dc8222 (patch) | |
| tree | 295792fd05c66c9f48e09ecd8525a694501b5000 /proofs/NectarDriver | |
| parent | 8769270744d26e8884cc819bc86c5f5514be5c78 (diff) | |
chore: Fix scope leakage problem, adding proofs to NectarDriver.
Signed-off-by: Amlal El Mahrouss <amlal@nekernel.org>
Diffstat (limited to 'proofs/NectarDriver')
| -rw-r--r-- | proofs/NectarDriver/Impl.v | 11 | ||||
| -rw-r--r-- | proofs/NectarDriver/Traits.v | 10 |
2 files changed, 21 insertions, 0 deletions
diff --git a/proofs/NectarDriver/Impl.v b/proofs/NectarDriver/Impl.v new file mode 100644 index 0000000..37b8878 --- /dev/null +++ b/proofs/NectarDriver/Impl.v @@ -0,0 +1,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.
\ No newline at end of file diff --git a/proofs/NectarDriver/Traits.v b/proofs/NectarDriver/Traits.v new file mode 100644 index 0000000..2c5bb9c --- /dev/null +++ b/proofs/NectarDriver/Traits.v @@ -0,0 +1,10 @@ +(* + NectarDriver: Traits keyword. + + The Traits keyword defines formal semantic rules associated with a specific identifier N. + + Author: Amlal El Mahrouss + Formalization: January 2026 +*) + +Require Import Logic.Classical_Prop. |