Skip to content

Instantly share code, notes, and snippets.

@llelf
Created April 28, 2020 01:06
Show Gist options
  • Save llelf/4b285466ab460c9d7b9b54b8144709f3 to your computer and use it in GitHub Desktop.
Save llelf/4b285466ab460c9d7b9b54b8144709f3 to your computer and use it in GitHub Desktop.
Module I32:=Int. Module I64:=Int64.
Notation i32:=I32.int. Notation i64:=I64.int.
Notation "[i32 i ]" := (I32.mkint i _)(format "[i32 i ]").
Notation "[i64 i ]" := (I64.mkint i _)(format "[i64 i ]").
Section core.
Inductive Nu := I of i32 | J of i64.
Inductive At := ANu of Nu | AC of ascii.
Inductive Ty := Ti|Tj|TL|Tc.
Unset Elimination Schemes.
Inductive K := A of At | L of Ty & nat & seq1 K.
Definition K_ind
(P: K->Prop)
(IA: forall a:At, P(A a))
(IL: forall (t:Ty)(n:nat)(a:K)(s:seq K),
foldr (fun x:K => and(P x)) True (a::s) -> P (L t n (NE.mk a s))) :=
fix loop a: P a: Prop := match a with
| A a => IA a
| L t n (NE.mk a0 s0) =>
let fix all s : foldr (fun x => and (P x)) True s :=
if s is e::s then conj (loop e) (all s) else Logic.I
in IL t n a0 s0 (all (a0::s0))
end. Set Elimination Schemes.
Definition nu2k n := A(ANu n). Coercion nu2k: Nu >-> K.
Definition nat2i32 n := I32.repr(Z.of_nat n). Coercion nat2i32: nat >-> i32.
Definition nat2i64 n := I64.repr(Z.of_nat n). Coercion nat2i64: nat >-> i64.
End core.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment