senvas/ladder-calculus
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

coq: notations for type terms

Browse source
This commit is contained in:
Michael Sippel 2024-07-27 13:28:52 +02:00
parent 13165a7951
commit d880e07d57
Signed by: senvas
GPG key ID: F96CF119C34B64A6
1 changed files with 30 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
coq/terms.v
View file

@ -36,10 +36,36 @@ Coercion type_var : string >-> type_term.
Coercion expr_var : string >-> expr_term.
(*
Notation "( x )" := x (at level 70).
Notation "x ~ y" := (type_rung x y) (at level 69, left associativity).
Notation "< x y >" := (type_app x y) (at level 68, left associativity).
Notation "'$' x" := (type_id x) (at level 66).
Coercion type_var : string >-> type_term.
Coercion expr_var : string >-> expr_term.
*)
Declare Scope ladder_type_scope.
Declare Scope ladder_expr_scope.
Declare Custom Entry ladder_type.
Notation "[ e ]" := e (e custom ladder_type at level 80) : ladder_type_scope.
(* TODO: allow any variable names in notation, not just α,β,γ *)
Notation "'∀α.' τ" := (type_univ "α" τ) (in custom ladder_type at level 80) : ladder_type_scope.
Notation "'∀β.' τ" := (type_univ "β" τ) (in custom ladder_type at level 80) : ladder_type_scope.
Notation "'∀γ.' τ" := (type_univ "γ" τ) (in custom ladder_type at level 80) : ladder_type_scope.
Notation "'<' σ τ '>'" := (type_spec σ τ) (in custom ladder_type at level 80, left associativity) : ladder_type_scope.
Notation "'(' τ ')'" := τ (in custom ladder_type at level 70) : ladder_type_scope.
Notation "σ '->' τ" := (type_fun σ τ) (in custom ladder_type at level 75, right associativity) : ladder_type_scope.
Notation "σ '->morph' τ" := (type_morph σ τ) (in custom ladder_type at level 75, right associativity) : ladder_type_scope.
Notation "σ '~' τ" := (type_ladder σ τ) (in custom ladder_type at level 70, right associativity) : ladder_type_scope.
Notation "'α'" := (type_var "α") (in custom ladder_type at level 60, right associativity) : ladder_type_scope.
Notation "'β'" := (type_var "β") (in custom ladder_type at level 60, right associativity) : ladder_type_scope.
Notation "'γ'" := (type_var "γ") (in custom ladder_type at level 60, right associativity) : ladder_type_scope.
Open Scope ladder_type_scope.
Definition t1 : type_term := [ ∀α.∀β.(α~β~γ)->β->(α->α)->β ].
Compute t1.
Close Scope ladder_type_scope.
End Terms.