Commit 4f7441e0 authored by Dan Frumin's avatar Dan Frumin

Forgot to add typetest

parent 61f69839
From iris_logrel.F_mu_ref_conc Require Import typing reflection.
Definition prog : val := λ: "x", if: !"x" then (λ: <>, 1) else (λ: <>, 0).
Lemma prog_typed Γ : Γ ⊢ₜ prog : TArrow (Tref TBool) (TArrow TUnit TNat).
Hint Resolve prog_typed : typeable.
Definition prog2 : val := λ: <>,
let: "x" := ref false in
prog "x" ().
Lemma prog2_typed Γ : Γ ⊢ₜ prog2 : TArrow TUnit TNat.
Proof. solve_typed. Qed.
Hint Resolve prog2_typed : typeable.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment