dtlc

dependently-typed lambda calculus toy
git clone git://git.rr3.xyz/dtlc
Log | Files | Refs | README | LICENSE

commit 54013f815d85edede36ea27876f82d5de84ee46e
parent 2c7eb0844adceb5e16dd5b83583293438c1c3914
Author: Robert Russell <robertrussell.72001@gmail.com>
Date:   Tue, 30 Jan 2024 04:24:41 -0800

Move some eval code

Diffstat:
DTODO.txt | 0
Meval.ml | 6+++---
2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/TODO.txt b/TODO.txt diff --git a/eval.ml b/eval.ml @@ -16,6 +16,9 @@ let rec define_data_args impossible "Eval.define_data_args: value and disc have different tag" end; let tagi = v.tagi in + let (_, {I.ctors; _}) = v.datatype_clo in + let vorder = ctors.(tagi).order in + let dorder = d.datatype.ctors.(tagi).order in begin if Array.length v.args <> Array.length d.subpatts then impossible "Eval.define_data_args: value and disc have different arity" @@ -26,9 +29,6 @@ let rec define_data_args let env = Env.bind env subvars in let env = ref env in for i = 0 to arity - 1 do - let (_, {I.ctors; _}) = v.datatype_clo in - let vorder = ctors.(tagi).order in - let dorder = d.datatype.ctors.(tagi).order in begin if vorder.(i) <> dorder.(i) then impossible "Eval.define_data_args: value and disc have different order" end;