1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
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).
|
