▽天泣記
●03/22 12:45
2025-03-20 (Thu)#1 あみだくじ (2)証明の場合分けが不必要に多かったので減らしてみた｡(他にもいくらか調整した｡)From mathcomp Require Import all_ssreflect.Section amida_kuji.Variable segment : eqType.Definition path := seq segment.(* amida-kuji has determinstic function to obtain next segment *)Variable next : segment -> option segment.Definition valid_path (seg : segment) (p : path) : bool := all id (pairmap (fun x y => next x =