Commit 2224eaf2 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove hack.

parent 6ce58f78
From iris.heap_lang Require Export proofmode notation. From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import assert. From iris.heap_lang Require Import assert.
Opaque Z.of_nat.
(** Immutable ML-style functional lists *) (** Immutable ML-style functional lists *)
Fixpoint is_list (hd : val) (xs : list val) : Prop := Fixpoint is_list (hd : val) (xs : list val) : Prop :=
match xs with match xs with
......
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