Add unproven lemma about fold implication
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
8ff88f9f9e
commit
f0b0d51b48
|
@ -247,6 +247,10 @@ module WithProg (prog : Program) where
|
||||||
in
|
in
|
||||||
⟦⟧ˡ-respects-≈ˡ (≈ˡ-sym l≈l') v ⟦l'⟧v
|
⟦⟧ˡ-respects-≈ˡ (≈ˡ-sym l≈l') v ⟦l'⟧v
|
||||||
|
|
||||||
|
⟦⟧ᵛ-foldr : ∀ {vs : VariableValues} {vss : List VariableValues} {ρ : Env} →
|
||||||
|
⟦ vs ⟧ᵛ ρ → vs ∈ˡ vss → ⟦ foldr _⊔ᵛ_ ⊥ᵛ vss ⟧ᵛ ρ
|
||||||
|
⟦⟧ᵛ-foldr = {!!}
|
||||||
|
|
||||||
InterpretationValid : Set
|
InterpretationValid : Set
|
||||||
InterpretationValid = ∀ {vs ρ e v} → ρ , e ⇒ᵉ v → ⟦ vs ⟧ᵛ ρ → ⟦ eval e vs ⟧ˡ v
|
InterpretationValid = ∀ {vs ρ e v} → ρ , e ⇒ᵉ v → ⟦ vs ⟧ᵛ ρ → ⟦ eval e vs ⟧ˡ v
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue
Block a user