<commit_before>/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Module: general_notation
Authors: <NAME>, <NAME>
-/
prelude
import init.datatypes

notation `assume` binders `,` r:(scoped f, f) := r
notation `take`   binders `,` r:(scoped f, f) := r

/-
  Global declarations of right binding strength

  If a module reassigns these, it will be incompatible with other modules that adhere to these
  conventions.

  When hovering over a symbol, use "C-u C-x =" to see how to input it.
-/

/- Logical operations and relations -/

definition std.prec.max   : num := 1024 -- reflects max precedence used internally
definition std.prec.arrow : num := 25

reserve prefix `¬`:40
reserve prefix `~`:40
reserve infixr `∧`:35
reserve infixr `/\`:35
reserve infixr `‌\/`:30
reserve infixr `∨`:30
reserve infix `<->`:25
reserve infix `↔`:25
reserve infix `=`:50
reserve infix `≠`:50
reserve infix `≈`:50
reserve infix `∼`:50
<commit_msg>fix(init/reserved_notation): remove "invisible" character at `\/`<commit_after>/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Module: general_notation
Authors: <NAME>, <NAME>
-/
prelude
import init.datatypes

notation `assume` binders `,` r:(scoped f, f) := r
notation `take`   binders `,` r:(scoped f, f) := r

/-
  Global declarations of right binding strength

  If a module reassigns these, it will be incompatible with other modules that adhere to these
  conventions.

  When hovering over a symbol, use "C-u C-x =" to see how to input it.
-/

/- Logical operations and relations -/

definition std.prec.max   : num := 1024 -- reflects max precedence used internally
definition std.prec.arrow : num := 25

reserve prefix `¬`:40
reserve prefix `~`:40
reserve infixr `∧`:35
reserve infixr `/\`:35
reserve infixr `\/`:30
reserve infixr `∨`:30
reserve infix `<->`:25
reserve infix `↔`:25
reserve infix `=`:50
reserve infix `≠`:50
reserve infix `≈`:50
reserve infix `∼`:50

{'fraction_non_alphanumeric': 0.12493970091654606, 'fraction_numerical': 0.03473227206946455, 'mean_word_length': 4.0958230958230954, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 9, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7468620', 'n_tokens_mistral': 782, 'n_tokens_neox': 688, 'n_words': 269}