open import Definition.Typed.Restrictions
open import Graded.Modality
module Definition.Typechecking.Deterministic
{a} {M : Set a}
{š : Modality M}
(R : Type-restrictions š)
where
open import Definition.Typechecking R
open import Definition.Typed R
open import Definition.Typed.Properties R
open import Definition.Untyped M
open import Tools.Fin
open import Tools.Nat
open import Tools.Product
import Tools.PropositionalEquality as PE
private
variable
n : Nat
t A B : Term n
Ī : Con Term n
deterministicā-var : {x : Fin n} ā x ā· A ā Ī ā x ā· B ā Ī ā A PE.ā” B
deterministicā-var {x = x0} here here = PE.refl
deterministicā-var {x = x +1} (there y) (there z) rewrite deterministicā-var y z = PE.refl
deterministicā : Ī ā¢ t ā A ā Ī ā¢ t ā B ā A PE.ā” B
deterministicā (Ī Ī£įµ¢ _ _ _) (Ī Ī£įµ¢ _ _ _) = PE.refl
deterministicā (varįµ¢ x) (varįµ¢ xā) = deterministicā-var x xā
deterministicā (appįµ¢ x xā xā) (appįµ¢ y xā xā)
rewrite deterministicā x y
with B-PE-injectivity BĪ ! BĪ ! (whrDet* xā xā)
... | PE.refl , PE.refl , _ = PE.refl
deterministicā (fstįµ¢ x xā) (fstįµ¢ y xā)
rewrite deterministicā x y
with B-PE-injectivity BĪ£! BĪ£! (whrDet* xā xā)
... | PE.refl , PE.refl , _ = PE.refl
deterministicā (sndįµ¢ x xā) (sndįµ¢ y xā)
rewrite deterministicā x y
with B-PE-injectivity BĪ£! BĪ£! (whrDet* xā xā)
... | PE.refl , PE.refl , _ = PE.refl
deterministicā (prodrecįµ¢ _ _ _ _) (prodrecįµ¢ _ _ _ _) = PE.refl
deterministicā āįµ¢ āįµ¢ = PE.refl
deterministicā zeroįµ¢ zeroįµ¢ = PE.refl
deterministicā (sucįµ¢ x) (sucįµ¢ xā) = PE.refl
deterministicā (natrecįµ¢ x xā xā xā) (natrecįµ¢ xā xā
xā xā) = PE.refl
deterministicā (Unitįµ¢ _) (Unitįµ¢ _) = PE.refl
deterministicā (starįµ¢ _) (starįµ¢ _) = PE.refl
deterministicā (unitrecįµ¢ _ _ _) (unitrecįµ¢ _ _ _) = PE.refl
deterministicā Emptyįµ¢ Emptyįµ¢ = PE.refl
deterministicā (emptyrecįµ¢ x xā) (emptyrecįµ¢ xā xā) = PE.refl
deterministicā (Idįµ¢ _ _ _) (Idįµ¢ _ _ _) = PE.refl
deterministicā (Jįµ¢ _ _ _ _ _ _) (Jįµ¢ _ _ _ _ _ _) = PE.refl
deterministicā (Kįµ¢ _ _ _ _ _ _) (Kįµ¢ _ _ _ _ _ _) = PE.refl
deterministicā ([]-congįµ¢ _ _ _ _ _) ([]-congįµ¢ _ _ _ _ _) = PE.refl