MATCH_CONV : term -> thm
# MATCH_CONV `match [1;2;3;4;5] with CONS x (CONS y z) -> z`;; val it : thm = |- (match [1; 2; 3; 4; 5] with CONS x (CONS y z) -> z) = [3; 4; 5]
# MATCH_CONV `(function [] -> 0 | CONS h t -> h + 1) [1;2;3;4]`;; val it : thm = |- (function [] -> 0 | CONS h t -> h + 1) [1; 2; 3; 4] = (function CONS h t -> h + 1) [1; 2; 3; 4]
# TOP_DEPTH_CONV MATCH_CONV `(function [] -> 0 | CONS h t -> h + 1) [1;2;3;4]`;; val it : thm = |- (function [] -> 0 | CONS h t -> h + 1) [1; 2; 3; 4] = 1 + 1
# MATCH_CONV `(function [] -> 0 | CONS h t -> h + 1) l`;; val it : thm = |- (function [] -> 0 | CONS h t -> h + 1) l = (if [] = l then (function [] -> 0) l else (function CONS h t -> h + 1) l)
# REWRITE_CONV[] `match [1;2;3] with CONS h t when h = 1 -> h + LENGTH t`;; val it : thm = |- (match [1; 2; 3] with CONS h t when h = 1 -> h + LENGTH t) = 1 + LENGTH [2; 3] # REWRITE_CONV[] `match [1;2;3] with CONS h t when h < 7 -> h + LENGTH t`;; val it : thm = |- (match [1; 2; 3] with CONS h t when h < 7 -> h + LENGTH t) = (match [1; 2; 3] with CONS h t when h < 7 -> h + LENGTH t)