1. Paweł Wieczorek
  2. MgrCoq

Commits

Paweł Wieczorek  committed 713e64c

added weird rule

  • Participants
  • Parent commits a7cfd25
  • Branches weird_rule

Comments (0)

Files changed (1)

File Nbe/Syntax/System.v

View file
 | FUN_E: forall Gamma M N A B,
   Gamma |-- M : TmFun A B ->
   Gamma |-- N : A ->
+  Gamma,, A |-- B ->
   Gamma |-- TmApp M N : TmSb B (Ssing N)
 
 | FUN_I: forall Gamma M A B,