Skip to content

chore(spdx): add Copyright (c) headers to Idris2 files (batch 5/7) #100

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 1 commit into from
Jun 1, 2026
Merged

chore(spdx): add Copyright (c) headers to Idris2 files (batch 5/7) #100

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions alkahest-shell-transmuter/src/abi/Foreign.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
-- SPDX-License-Identifier: MPL-2.0
-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
||| Foreign Function Interface Declarations
|||
||| This module declares all C-compatible functions that will be
Expand Down
2 changes: 2 additions & 0 deletions alkahest-shell-transmuter/src/abi/Layout.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
-- SPDX-License-Identifier: MPL-2.0
-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
||| Memory Layout Proofs
|||
||| This module provides formal proofs about memory layout, alignment,
Expand Down
2 changes: 2 additions & 0 deletions alkahest-shell-transmuter/src/abi/Types.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
-- SPDX-License-Identifier: MPL-2.0
-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
||| ALKAHEST-SHELL-TRANSMUTER — ABI Type Definitions
|||
||| This module defines the Application Binary Interface for the Alkahest
Expand Down
1 change: 1 addition & 0 deletions proofs/idris2/src/Filesystem/Composition.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
-- SPDX-License-Identifier: MPL-2.0
-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-- Filesystem Composition - Operation Sequences and Undo/Redo
--
-- Proves that sequences of reversible operations are themselves reversible.
Expand Down
1 change: 1 addition & 0 deletions proofs/idris2/src/Filesystem/Model.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
-- SPDX-License-Identifier: MPL-2.0
-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-- Filesystem Model - Core Types and Definitions
--
-- This module defines the abstract filesystem model used throughout
Expand Down
1 change: 1 addition & 0 deletions proofs/idris2/src/Filesystem/Operations.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
-- SPDX-License-Identifier: MPL-2.0
-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-- Filesystem Operations - mkdir, rmdir, touch, rm
--
-- All operations are total (guaranteed to terminate) and proven
Expand Down
1 change: 1 addition & 0 deletions proofs/idris2/src/Filesystem/RMO.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
-- SPDX-License-Identifier: MPL-2.0
-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-- RMO (Remove-Match-Obliterate) - Irreversible Operations
--
-- Implements GDPR "right to be forgotten" with mathematical guarantees.
Expand Down
1 change: 1 addition & 0 deletions src/abi/Foreign.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
||| SPDX-License-Identifier: MPL-2.0
-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
||| Foreign Function Interface Declarations for VALENCE_SHELL
|||
||| This module declares all C-compatible functions that will be
Expand Down
1 change: 1 addition & 0 deletions src/abi/Layout.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
-- SPDX-License-Identifier: MPL-2.0
-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
||| Memory Layout Proofs — ABI Foundation.
|||
||| This module provides the formal proofs required to ensure that
Expand Down
1 change: 1 addition & 0 deletions src/abi/Types.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
-- SPDX-License-Identifier: MPL-2.0
-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
||| VALENCE-SHELL (vsh) — ABI Type Definitions
|||
||| This module defines the Application Binary Interface for the Valence Shell.
Expand Down
Loading