other
_ < _ <= _ (bigN_scope) [notation, in :bigN_scope:x_'<'_x_'<='_x]
1 (bigN_scope) [notation, in :bigN_scope:'1']
_ <= _ (bigN_scope) [notation, in :bigN_scope:x_'<='_x]
_ ^ _ (bigN_scope) [notation, in :bigN_scope:x_'^'_x]
_ =? _ (bigN_scope) [notation, in :bigN_scope:x_'=?'_x]
_ <= _ <= _ (bigN_scope) [notation, in :bigN_scope:x_'<='_x_'<='_x]
2 (bigN_scope) [notation, in :bigN_scope:'2']
_ < _ < _ (bigN_scope) [notation, in :bigN_scope:x_'<'_x_'<'_x]
_ <= _ < _ (bigN_scope) [notation, in :bigN_scope:x_'<='_x_'<'_x]
_ > _ (bigN_scope) [notation, in :bigN_scope:x_'>'_x]
_ < _ (bigN_scope) [notation, in :bigN_scope:x_'<'_x]
_ != _ (bigN_scope) [notation, in :bigN_scope:x_'!='_x]
_ / _ (bigN_scope) [notation, in :bigN_scope:x_'/'_x]
0 (bigN_scope) [notation, in :bigN_scope:'0']
_ _ (bigN_scope) [notation, in :bigN_scope:x_''_x]
_ + _ (bigN_scope) [notation, in :bigN_scope:x_'+'_x]
_ ?= _ (bigN_scope) [notation, in :bigN_scope:x_'?='_x]
_ mod _ (bigN_scope) [notation, in :bigN_scope:x_'mod'_x]
_ >= _ (bigN_scope) [notation, in :bigN_scope:x_'>='_x]
_ * _ (bigN_scope) [notation, in :bigN_scope:x_'*'_x]
_ <=? _ (bigN_scope) [notation, in :bigN_scope:x_'<=?'_x]
[ _ ] (bigN_scope) [notation, in :bigN_scope:'['_x_']']
_ == _ (bigN_scope) [notation, in :bigN_scope:x_'=='_x]
_ - _ (bigN_scope) [notation, in :bigN_scope:x_'-'_x]
_ > _ (bigQ_scope) [notation, in :bigQ_scope:x_'>'_x]
_ < _ <= _ (bigQ_scope) [notation, in :bigQ_scope:x_'<'_x_'<='_x]
_ <= _ < _ (bigQ_scope) [notation, in :bigQ_scope:x_'<='_x_'<'_x]
_ < _ (bigQ_scope) [notation, in :bigQ_scope:x_'<'_x]
1 (bigQ_scope) [notation, in :bigQ_scope:'1']
[ _ ] (bigQ_scope) [notation, in :bigQ_scope:'['_x_']']
_ # _ (bigQ_scope) [notation, in :bigQ_scope:x_'#'_x]
_ + _ (bigQ_scope) [notation, in :bigQ_scope:x_'+'_x]
_ <= _ (bigQ_scope) [notation, in :bigQ_scope:x_'<='_x]
_ == _ (bigQ_scope) [notation, in :bigQ_scope:x_'=='_x]
_ < _ < _ (bigQ_scope) [notation, in :bigQ_scope:x_'<'_x_'<'_x]
_ ^ _ (bigQ_scope) [notation, in :bigQ_scope:x_'^'_x]
_ >= _ (bigQ_scope) [notation, in :bigQ_scope:x_'>='_x]
_ != _ (bigQ_scope) [notation, in :bigQ_scope:x_'!='_x]
0 (bigQ_scope) [notation, in :bigQ_scope:'0']
_ / _ (bigQ_scope) [notation, in :bigQ_scope:x_'/'_x]
_ * _ (bigQ_scope) [notation, in :bigQ_scope:x_'*'_x]
_ - _ (bigQ_scope) [notation, in :bigQ_scope:x_'-'_x]
_ <= _ <= _ (bigQ_scope) [notation, in :bigQ_scope:x_'<='_x_'<='_x]
_ ?= _ (bigQ_scope) [notation, in :bigQ_scope:x_'?='_x]
- _ (bigQ_scope) [notation, in :bigQ_scope:'-'_x]
_ == _ (bigZ_scope) [notation, in :bigZ_scope:x_'=='_x]
_ > _ (bigZ_scope) [notation, in :bigZ_scope:x_'>'_x]
_ <= _ <= _ (bigZ_scope) [notation, in :bigZ_scope:x_'<='_x_'<='_x]
_ / _ (bigZ_scope) [notation, in :bigZ_scope:x_'/'_x]
_ <= _ (bigZ_scope) [notation, in :bigZ_scope:x_'<='_x]
_ ^ _ (bigZ_scope) [notation, in :bigZ_scope:x_'^'_x]
0 (bigZ_scope) [notation, in :bigZ_scope:'0']
_ _ (bigZ_scope) [notation, in :bigZ_scope:x_''_x]
_ < _ (bigZ_scope) [notation, in :bigZ_scope:x_'<'_x]
_ mod _ (bigZ_scope) [notation, in :bigZ_scope:x_'mod'_x]
_ ?= _ (bigZ_scope) [notation, in :bigZ_scope:x_'?='_x]
_ <= _ < _ (bigZ_scope) [notation, in :bigZ_scope:x_'<='_x_'<'_x]
_ - _ (bigZ_scope) [notation, in :bigZ_scope:x_'-'_x]
_ + _ (bigZ_scope) [notation, in :bigZ_scope:x_'+'_x]
- _ (bigZ_scope) [notation, in :bigZ_scope:'-'_x]
_ * _ (bigZ_scope) [notation, in :bigZ_scope:x_'*'_x]
_ ÷ _ (bigZ_scope) [notation, in :bigZ_scope:x_'÷'_x]
_ <=? _ (bigZ_scope) [notation, in :bigZ_scope:x_'<=?'_x]
1 (bigZ_scope) [notation, in :bigZ_scope:'1']
_ != _ (bigZ_scope) [notation, in :bigZ_scope:x_'!='_x]
_ >= _ (bigZ_scope) [notation, in :bigZ_scope:x_'>='_x]
[ _ ] (bigZ_scope) [notation, in :bigZ_scope:'['_x_']']
_ =? _ (bigZ_scope) [notation, in :bigZ_scope:x_'=?'_x]
_ < _ < _ (bigZ_scope) [notation, in :bigZ_scope:x_'<'_x_'<'_x]
_ < _ <= _ (bigZ_scope) [notation, in :bigZ_scope:x_'<'_x_'<='_x]
2 (bigZ_scope) [notation, in :bigZ_scope:'2']
_ && _ (bool_scope) [notation, in :bool_scope:x_'&&'_x]
_ || _ (bool_scope) [notation, in :bool_scope:x_'||'_x]
( _ , _ , .. , _ ) (core_scope) [notation, in :core_scope:'('_x_','_x_','_'..'_','_x_')']
_ === _ (equiv_scope) [notation, in :equiv_scope:x_'==='_x]
_ =/= _ (equiv_scope) [notation, in :equiv_scope:x_'=/='_x]
_ =~= _ (equiv_scope) [notation, in :equiv_scope:x_'=~='_x]
_ == _ (equiv_scope) [notation, in :equiv_scope:x_'=='_x]
_ <> _ (equiv_scope) [notation, in :equiv_scope:x_'<>'_x]
_ -c _ (int31_scope) [notation, in :int31_scope:x_'-c'_x]
_ - _ (int31_scope) [notation, in :int31_scope:x_'-'_x]
_ * _ (int31_scope) [notation, in :int31_scope:x_'*'_x]
_ *c _ (int31_scope) [notation, in :int31_scope:x_'*c'_x]
- _ (int31_scope) [notation, in :int31_scope:'-'_x]
_ ?= _ (int31_scope) [notation, in :int31_scope:x_'?='_x]
_ +c _ (int31_scope) [notation, in :int31_scope:x_'+c'_x]
_ + _ (int31_scope) [notation, in :int31_scope:x_'+'_x]
_ / _ (int31_scope) [notation, in :int31_scope:x_'/'_x]
_ &&& _ (lazy_bool_scope) [notation, in :lazy_bool_scope:x_'&&&'_x]
_ ||| _ (lazy_bool_scope) [notation, in :lazy_bool_scope:x_'|||'_x]
_ :: _ (list_scope) [notation, in :list_scope:x_'::'_x]
_ ++ _ (list_scope) [notation, in :list_scope:x_'++'_x]
_ <= _ (nat_scope) [notation, in :nat_scope:x_'<='_x]
_ _ (nat_scope) [notation, in :nat_scope:x_''_x]
_ mod _ (nat_scope) [notation, in :nat_scope:x_'mod'_x]
( _ | _ ) (nat_scope) [notation, in :nat_scope:'('_x_'|'_x_')']
_ / _ (nat_scope) [notation, in :nat_scope:x_'/'_x]
_ >= _ (nat_scope) [notation, in :nat_scope:x_'>='_x]
_ <= _ <= _ (nat_scope) [notation, in :nat_scope:x_'<='_x_'<='_x]
_ > _ (nat_scope) [notation, in :nat_scope:x_'>'_x]
_ < _ < _ (nat_scope) [notation, in :nat_scope:x_'<'_x_'<'_x]
_ <= _ < _ (nat_scope) [notation, in :nat_scope:x_'<='_x_'<'_x]
_ < _ (nat_scope) [notation, in :nat_scope:x_'<'_x]
_ * _ (nat_scope) [notation, in :nat_scope:x_'*'_x]
_ + _ (nat_scope) [notation, in :nat_scope:x_'+'_x]
_ < _ <= _ (nat_scope) [notation, in :nat_scope:x_'<'_x_'<='_x]
_ - _ (nat_scope) [notation, in :nat_scope:x_'-'_x]
_ ^ _ (nat_scope) [notation, in :nat_scope:x_'^'_x]
_ <=? _ (nat_scope) [notation, in :nat_scope:x_'<=?'_x]
_ <= _ < _ (N_scope) [notation, in :N_scope:x_'<='_x_'<'_x]
_ <= _ (N_scope) [notation, in :N_scope:x_'<='_x]
_ * _ (N_scope) [notation, in :N_scope:x_'*'_x]
_ - _ (N_scope) [notation, in :N_scope:x_'-'_x]
_ mod _ (N_scope) [notation, in :N_scope:x_'mod'_x]
_ / _ (N_scope) [notation, in :N_scope:x_'/'_x]
_ ?= _ (N_scope) [notation, in :N_scope:x_'?='_x]
_ >= _ (N_scope) [notation, in :N_scope:x_'>='_x]
_ < _ < _ (N_scope) [notation, in :N_scope:x_'<'_x_'<'_x]
( _ | _ ) (N_scope) [notation, in :N_scope:'('_x_'|'_x_')']
_ ^ _ (N_scope) [notation, in :N_scope:x_'^'_x]
_ <=? _ (N_scope) [notation, in :N_scope:x_'<=?'_x]
_ _ (N_scope) [notation, in :N_scope:x_''_x]
_ =? _ (N_scope) [notation, in :N_scope:x_'=?'_x]
_ < _ (N_scope) [notation, in :N_scope:x_'<'_x]
_ + _ (N_scope) [notation, in :N_scope:x_'+'_x]
_ < _ <= _ (N_scope) [notation, in :N_scope:x_'<'_x_'<='_x]
_ <= _ <= _ (N_scope) [notation, in :N_scope:x_'<='_x_'<='_x]
_ > _ (N_scope) [notation, in :N_scope:x_'>'_x]
_ #2 (pair_scope) [notation, in :pair_scope:x_'#2']
_ #2 (pair_scope) [notation, in :pair_scope:x_'#2']
_ #1 (pair_scope) [notation, in :pair_scope:x_'#1']
_ #1 (pair_scope) [notation, in :pair_scope:x_'#1']
( _ | _ ) (positive_scope) [notation, in :positive_scope:'('_x_'|'_x_')']
_ ?= _ (positive_scope) [notation, in :positive_scope:x_'?='_x]
_ ~ 1 (positive_scope) [notation, in :positive_scope:x_'~'_'1']
_ =? _ (positive_scope) [notation, in :positive_scope:x_'=?'_x]
_ >= _ (positive_scope) [notation, in :positive_scope:x_'>='_x]
_ > _ (positive_scope) [notation, in :positive_scope:x_'>'_x]
_ - _ (positive_scope) [notation, in :positive_scope:x_'-'_x]
_ < _ <= _ (positive_scope) [notation, in :positive_scope:x_'<'_x_'<='_x]
_ * _ (positive_scope) [notation, in :positive_scope:x_'*'_x]
_ < _ < _ (positive_scope) [notation, in :positive_scope:x_'<'_x_'<'_x]
_ <= _ <= _ (positive_scope) [notation, in :positive_scope:x_'<='_x_'<='_x]
_ <=? _ (positive_scope) [notation, in :positive_scope:x_'<=?'_x]
_ + _ (positive_scope) [notation, in :positive_scope:x_'+'_x]
_ ~ 0 (positive_scope) [notation, in :positive_scope:x_'~'_'0']
_ <= _ < _ (positive_scope) [notation, in :positive_scope:x_'<='_x_'<'_x]
_ _ (positive_scope) [notation, in :positive_scope:x_''_x]
_ ^ _ (positive_scope) [notation, in :positive_scope:x_'^'_x]
_ <= _ (positive_scope) [notation, in :positive_scope:x_'<='_x]
_ < _ (positive_scope) [notation, in :positive_scope:x_'<'_x]
_ <∙> _ (predicate_scope) [notation, in :predicate_scope:x_'<∙>'_x]
_ \∙/ _ (predicate_scope) [notation, in :predicate_scope:x_'\∙/'_x]
_ -∙> _ (predicate_scope) [notation, in :predicate_scope:x_'-∙>'_x]
∙⊥∙ (predicate_scope) [notation, in :predicate_scope:'∙⊥∙']
_ /∙\ _ (predicate_scope) [notation, in :predicate_scope:x_'/∙\'_x]
∙⊤∙ (predicate_scope) [notation, in :predicate_scope:'∙⊤∙']
! (program_scope) [notation, in :program_scope:'!']
_ `= _ (program_scope) [notation, in :program_scope:x_'`='_x]
` _ (program_scope) [notation, in :program_scope:'`'_x]
_ ∘ _ (program_scope) [notation, in :program_scope:x_'∘'_x]
_ >= _ (Qc_scope) [notation, in :Qc_scope:x_'>='_x]
_ <= _ <= _ (Qc_scope) [notation, in :Qc_scope:x_'<='_x_'<='_x]
1 (Qc_scope) [notation, in :Qc_scope:'1']
_ * _ (Qc_scope) [notation, in :Qc_scope:x_'*'_x]
- _ (Qc_scope) [notation, in :Qc_scope:'-'_x]
_ - _ (Qc_scope) [notation, in :Qc_scope:x_'-'_x]
_ ?= _ (Qc_scope) [notation, in :Qc_scope:x_'?='_x]
_ <= _ (Qc_scope) [notation, in :Qc_scope:x_'<='_x]
_ / _ (Qc_scope) [notation, in :Qc_scope:x_'/'_x]
0 (Qc_scope) [notation, in :Qc_scope:'0']
!! (Qc_scope) [notation, in :Qc_scope:'!!']
/ _ (Qc_scope) [notation, in :Qc_scope:'/'_x]
_ < _ (Qc_scope) [notation, in :Qc_scope:x_'<'_x]
_ < _ < _ (Qc_scope) [notation, in :Qc_scope:x_'<'_x_'<'_x]
_ > _ (Qc_scope) [notation, in :Qc_scope:x_'>'_x]
_ + _ (Qc_scope) [notation, in :Qc_scope:x_'+'_x]
_ ^ _ (Qc_scope) [notation, in :Qc_scope:x_'^'_x]
_ - _ (Q_scope) [notation, in :Q_scope:x_'-'_x]
_ ?= _ (Q_scope) [notation, in :Q_scope:x_'?='_x]
_ == _ (Q_scope) [notation, in :Q_scope:x_'=='_x]
_ < _ (Q_scope) [notation, in :Q_scope:x_'<'_x]
_ # _ (Q_scope) [notation, in :Q_scope:x_'#'_x]
1 (Q_scope) [notation, in :Q_scope:'1']
_ <= _ <= _ (Q_scope) [notation, in :Q_scope:x_'<='_x_'<='_x]
_ > _ (Q_scope) [notation, in :Q_scope:x_'>'_x]
_ * _ (Q_scope) [notation, in :Q_scope:x_'*'_x]
/ _ (Q_scope) [notation, in :Q_scope:'/'_x]
0 (Q_scope) [notation, in :Q_scope:'0']
- _ (Q_scope) [notation, in :Q_scope:'-'_x]
_ ^ _ (Q_scope) [notation, in :Q_scope:x_'^'_x]
_ + _ (Q_scope) [notation, in :Q_scope:x_'+'_x]
_ >= _ (Q_scope) [notation, in :Q_scope:x_'>='_x]
_ / _ (Q_scope) [notation, in :Q_scope:x_'/'_x]
_ <= _ (Q_scope) [notation, in :Q_scope:x_'<='_x]
- _ (Rfun_scope) [notation, in :Rfun_scope:'-'_x]
_ - _ (Rfun_scope) [notation, in :Rfun_scope:x_'-'_x]
/ _ (Rfun_scope) [notation, in :Rfun_scope:'/'_x]
_ * _ (Rfun_scope) [notation, in :Rfun_scope:x_'*'_x]
_ o _ (Rfun_scope) [notation, in :Rfun_scope:x_'o'_x]
_ / _ (Rfun_scope) [notation, in :Rfun_scope:x_'/'_x]
_ + _ (Rfun_scope) [notation, in :Rfun_scope:x_'+'_x]
_ < _ <= _ (R_scope) [notation, in :R_scope:x_'<'_x_'<='_x]
_ ^Z _ (R_scope) [notation, in :R_scope:x_'^Z'_x]
_ / _ (R_scope) [notation, in :R_scope:x_'/'_x]
_ ^R _ (R_scope) [notation, in :R_scope:x_'^R'_x]
/ _ (R_scope) [notation, in :R_scope:'/'_x]
_ ^ _ (R_scope) [notation, in :R_scope:x_'^'_x]
- _ (R_scope) [notation, in :R_scope:'-'_x]
_ < _ (R_scope) [notation, in :R_scope:x_'<'_x]
_ <= _ (R_scope) [notation, in :R_scope:x_'<='_x]
_ * _ (R_scope) [notation, in :R_scope:x_'*'_x]
_ > _ (R_scope) [notation, in :R_scope:x_'>'_x]
_ >= _ (R_scope) [notation, in :R_scope:x_'>='_x]
_ < _ < _ (R_scope) [notation, in :R_scope:x_'<'_x_'<'_x]
_ + _ (R_scope) [notation, in :R_scope:x_'+'_x]
_ <= _ < _ (R_scope) [notation, in :R_scope:x_'<='_x_'<'_x]
_ ² (R_scope) [notation, in :R_scope:x_'²']
_ - _ (R_scope) [notation, in :R_scope:x_'-'_x]
_ <= _ <= _ (R_scope) [notation, in :R_scope:x_'<='_x_'<='_x]
_ @@1 (signature_scope) [notation, in :signature_scope:x_'@@1']
_ @@ _ (signature_scope) [notation, in :signature_scope:x_'@@'_x]
_ * _ (signature_scope) [notation, in :signature_scope:x_'*'_x]
_ @@2 (signature_scope) [notation, in :signature_scope:x_'@@2']
_ ++ _ (string_scope) [notation, in :string_scope:x_'++'_x]
_ → _ (type_scope) [notation, in :type_scope:x_'→'_x]
_ ^ _ (type_scope) [notation, in :type_scope:x_'^'_x]
exists2 _ : _ , _ & _ (type_scope) [notation, in :type_scope:'exists2'_x_':'_x_','_x_'&'_x]
_ = _ (type_scope) [notation, in :type_scope:x_'='_x]
~ _ (type_scope) [notation, in :type_scope:'~'_x]
{ _ | _ & _ } (type_scope) [notation, in :type_scope:'{'_x_'|'_x_'&'_x_'}']
∃ _ .. _ , _ (type_scope) [notation, in :type_scope:'∃'_x_'..'_x_','_x]
_ ^^ _ --> _ (type_scope) [notation, in :type_scope:x_'^^'_x_'-->'_x]
{ _ : _ & _ & _ } (type_scope) [notation, in :type_scope:'{'_x_':'_x_'&'_x_'&'_x_'}']
{ _ } + { _ } (type_scope) [notation, in :type_scope:'{'_x_'}'_'+'_'{'_x_'}']
exists ! _ .. _ , _ (type_scope) [notation, in :type_scope:'exists'_'!'_x_'..'_x_','_x]
_ ∨ _ (type_scope) [notation, in :type_scope:x_'∨'_x]
{ _ : _ | _ } (type_scope) [notation, in :type_scope:'{'_x_':'_x_'|'_x_'}']
_ ≠ _ (type_scope) [notation, in :type_scope:x_'≠'_x]
_ ↔ _ (type_scope) [notation, in :type_scope:x_'↔'_x]
¬ _ (type_scope) [notation, in :type_scope:'¬'_x]
_ + { _ } (type_scope) [notation, in :type_scope:x_'+'_'{'_x_'}']
{ _ : _ | _ & _ } (type_scope) [notation, in :type_scope:'{'_x_':'_x_'|'_x_'&'_x_'}']
_ \/ _ (type_scope) [notation, in :type_scope:x_'\/'_x]
_ * _ (type_scope) [notation, in :type_scope:x_'*'_x]
{ _ | _ } (type_scope) [notation, in :type_scope:'{'_x_'|'_x_'}']
{ _ : _ & _ } (type_scope) [notation, in :type_scope:'{'_x_':'_x_'&'_x_'}']
IF _ then _ else _ (type_scope) [notation, in :type_scope:'IF'_x_'then'_x_'else'_x]
_ <-> _ (type_scope) [notation, in :type_scope:x_'<->'_x]
exists _ .. _ , _ (type_scope) [notation, in :type_scope:'exists'_x_'..'_x_','_x]
() (type_scope) [notation, in :type_scope:'()']
_ = _ :> _ (type_scope) [notation, in :type_scope:x_'='_x_':>'_x]
_ <> _ :> _ (type_scope) [notation, in :type_scope:x_'<>'_x_':>'_x]
exists2 _ , _ & _ (type_scope) [notation, in :type_scope:'exists2'_x_','_x_'&'_x]
_ + _ (type_scope) [notation, in :type_scope:x_'+'_x]
_ =~= _ (type_scope) [notation, in :type_scope:x_'=~='_x]
_ ∧ _ (type_scope) [notation, in :type_scope:x_'∧'_x]
_ == _ (type_scope) [notation, in :type_scope:x_'=='_x]
{ ( _ , _ ) : _ | _ } (type_scope) [notation, in :type_scope:'{'_'('_x_','_x_')'_':'_x_'|'_x_'}']
_ /\ _ (type_scope) [notation, in :type_scope:x_'/\'_x]
_ =/= _ (type_scope) [notation, in :type_scope:x_'=/='_x]
∀ _ .. _ , _ (type_scope) [notation, in :type_scope:'∀'_x_'..'_x_','_x]
_ <> _ (type_scope) [notation, in :type_scope:x_'<>'_x]
_ < _ < _ (Z_scope) [notation, in :Z_scope:x_'<'_x_'<'_x]
_ >=? _ (Z_scope) [notation, in :Z_scope:x_'>=?'_x]
_ / _ (Z_scope) [notation, in :Z_scope:x_'/'_x]
_ > _ (Z_scope) [notation, in :Z_scope:x_'>'_x]
_ >= _ (Z_scope) [notation, in :Z_scope:x_'>='_x]
_ =? _ (Z_scope) [notation, in :Z_scope:x_'=?'_x]
_ + _ (Z_scope) [notation, in :Z_scope:x_'+'_x]
_ - _ (Z_scope) [notation, in :Z_scope:x_'-'_x]
_ ?= _ (Z_scope) [notation, in :Z_scope:x_'?='_x]
_ _ (Z_scope) [notation, in :Z_scope:x_''_x]
_ mod _ (Z_scope) [notation, in :Z_scope:x_'mod'_x]
_ ÷ _ (Z_scope) [notation, in :Z_scope:x_'÷'_x]
_ <= _ < _ (Z_scope) [notation, in :Z_scope:x_'<='_x_'<'_x]
_ <=? _ (Z_scope) [notation, in :Z_scope:x_'<=?'_x]
_ ^ _ (Z_scope) [notation, in :Z_scope:x_'^'_x]
( _ | _ ) (Z_scope) [notation, in :Z_scope:'('_x_'|'_x_')']
_ < _ <= _ (Z_scope) [notation, in :Z_scope:x_'<'_x_'<='_x]
_ >? _ (Z_scope) [notation, in :Z_scope:x_'>?'_x]
_ * _ (Z_scope) [notation, in :Z_scope:x_'*'_x]
_ ^^ _ (Z_scope) [notation, in :Z_scope:x_'^^'_x]
_ <= _ <= _ (Z_scope) [notation, in :Z_scope:x_'<='_x_'<='_x]
_ < _ (Z_scope) [notation, in :Z_scope:x_'<'_x]
- _ (Z_scope) [notation, in :Z_scope:'-'_x]
' _ (Z_scope) [notation, in :Z_scope:''''_x]
_ <= _ (Z_scope) [notation, in :Z_scope:x_'<='_x]
_ ^ _ [notation, in ::x_'^'_x]
_ ~= _ [notation, in ::x_'~='_x]
_ =_D _ [notation, in ::x_'=_D'_x]
_ == _ [notation, in ::x_'=='_x]
_ == _ [notation, in ::x_'=='_x]
_ ==b _ [notation, in ::x_'==b'_x]
_ ==b _ [notation, in ::x_'==b'_x]
_ << _ [notation, in ::x_'<<'_x]
_ << _ [notation, in ::x_'<<'_x]
_ :: _ [notation, in ::x_'::'_x]
_ :: _ [notation, in ::x_'::'_x]
_ <>b _ [notation, in ::x_'<>b'_x]
_ <>b _ [notation, in ::x_'<>b'_x]
_ =/= _ [notation, in ::x_'=/='_x]
_ ≥ _ [notation, in ::x_'≥'_x]
_ ≤ _ [notation, in ::x_'≤'_x]
_ + _ [notation, in ::x_'+'_x]
_ [@ _ ] [notation, in ::x_'[@'_x_']']
Set [notation, in ::'Set']
() [notation, in ::'()']
[ ] [notation, in ::'['_']']
[ ] [notation, in ::'['_']']
[ ] [notation, in ::'['_']']
[ ] [notation, in ::'['_']']
[ _ ; .. ; _ ] [notation, in ::'['_x_';'_'..'_';'_x_']']
[ _ ; .. ; _ ] [notation, in ::'['_x_';'_'..'_';'_x_']']
[ _ ; .. ; _ ] [notation, in ::'['_x_';'_'..'_';'_x_']']
[ _ ; .. ; _ ] [notation, in ::'['_x_';'_'..'_';'_x_']']
[] [notation, in ::'[]']
λ _ .. _ , _ [notation, in ::'λ'_x_'..'_x_','_x]