From ba61dfd69504ec6263a9dee9931d93adeb6f3142 Mon Sep 17 00:00:00 2001
From: Rutger Broekhoff
Date: Mon, 7 Jul 2025 21:52:08 +0200
Subject: Initialize repository

---
 theories/nix/notations.v | 43 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)
 create mode 100644 theories/nix/notations.v

(limited to 'theories/nix/notations.v')

diff --git a/theories/nix/notations.v b/theories/nix/notations.v
new file mode 100644
index 0000000..e9995b5
--- /dev/null
+++ b/theories/nix/notations.v
@@ -0,0 +1,43 @@
+From mininix Require Export nix.operational.
+
+(* Influenced by
+https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris_heap_lang/notation.v
+But always uses ":" instead of a scope. *)
+
+Coercion EId' : string >-> expr.
+Coercion NInt : Z >-> num.
+Coercion NFloat : float >-> num.
+Coercion LitNum : num >-> base_lit.
+Coercion LitBool : bool >-> base_lit.
+Coercion ELit : base_lit >-> expr.
+Coercion EApp : expr >-> Funclass.
+
+Notation "λattr: a , e" := (EAbsMatch a true e)
+  (at level 200, e, a at level 200,
+   format "'[' 'λattr:'  a  ,  '/  ' e ']'").
+Notation "λattr: a .., e" := (EAbsMatch a false e)
+  (at level 200, e, a at level 200,
+   format "'[' 'λattr:'  a  ..,  '/  ' e ']'").
+
+Notation "λ: x .. y , e" := (EAbs x .. (EAbs y e) ..)
+  (at level 200, x, y at level 1, e at level 200,
+   format "'[' 'λ:'  x  ..  y ,  '/  ' e ']'").
+Notation "'let:' x := e1 'in' e2" := (ELet x e1 e2)
+  (at level 200, x at level 1, e1, e2 at level 200,
+   format "'[' 'let:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'").
+Notation "'with:' a 'in' e" := (EWith a e)
+  (at level 200, a, e at level 200,
+   format "'[' 'with:'  a  'in'  '/' e ']'").
+
+Notation "'if:' e1 'then' e2 'else' e3" := (EIf e1 e2 e3)
+  (at level 200, e1, e2, e3 at level 200).
+
+Notation "e1 .: e2" := (ESelect e1 e2) (at level 70, no associativity).
+
+Notation "e1 +: e2" := (EBinOp AddOp e1 e2) (at level 50, left associativity).
+Notation "e1 *: e2" := (EBinOp MulOp e1 e2).
+Notation "e1 -: e2" := (EBinOp SubOp e1 e2) (at level 50, left associativity).
+Notation "e1 /: e2" := (EBinOp DivOp e1 e2) (at level 40).
+Notation "e1 =: e2" := (EBinOp EqOp e1 e2) (at level 70, no associativity).
+Notation "e1 <: e2" := (EBinOp LtOp e1 e2) (at level 70, no associativity).
+Notation "'ceil:' e" := (EBinOp (RoundOp Ceil) e LitNull) (at level 10).
-- 
cgit v1.2.3